theorem
proved
expr_induces_counted_once_combiner
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicAsFunctionalEquation.LinearLogicBridge on GitHub at line 78.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
75 ring
76
77/-- A counted-once resource expression induces a counted-once combiner. -/
78theorem expr_induces_counted_once_combiner
79 (e : CountedOnceResourceExpr) :
80 CountedOnceCombiner (fun u v => eval e u v) := by
81 exact counted_once_expr_biaffine e
82
83/-- Searchable alias: resource-linearity gives bi-affinity. -/
84theorem resource_linearity_gives_biaffinity
85 (e : CountedOnceResourceExpr) :
86 HasBiAffineForm e :=
87 counted_once_expr_biaffine e
88
89end CountedOnceResourceExpr
90
91end LogicAsFunctionalEquation
92end Foundation
93end IndisputableMonolith