packages feed

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 )