caledon-2.0.0.0: examples/coc.ncc

fixity lambda .λ
fixity lambda Π

defn tm : prop
   | p = tm
   | t = tm
   | .λ = tm → (tm → tm) → tm
   | Π = tm → (tm → tm) → tm

fixity none 0 ::
defn :: : tm -> tm -> prop
   | p_t = p :: t
   | lam_pi =  [A : tm][T : tm -> tm][B : tm -> tm]
      ([x] x :: A -> T x :: B x )
      -> (.λ x : A . T x) :: (Π x : A . B x)