caledon-2.0.0.0: examples/linear.ncc
defn trm : prop | lam = (trm -> trm) -> trm | app = trm -> trm -> trm defn linear : (trm -> trm) -> prop | linear_var = linear (λ V : trm . V )
defn trm : prop | lam = (trm -> trm) -> trm | app = trm -> trm -> trm defn linear : (trm -> trm) -> prop | linear_var = linear (λ V : trm . V )