caledon-2.0.0.0: examples/implicit.ncc

defn identity : prop -> prop
   | cons = {f : prop} f -> identity f

infix 1 =:=
defn =:= : {a : prop} a -> a -> prop
   | eq = {a : prop} a =:= a

defn getIdent : {f : prop} identity f -> f -> prop
  as ?\f : prop . \id : identity f . \v : f . (cons v) =:= id


-- this demonstrates three ways of doing this
defn getIdent' : {foo : prop} identity foo -> foo -> prop
   | getIdentity1 = {f}{V:f} getIdent' {foo = f} (cons V) V
   | getIdentity2 = {f}{V:f} getIdent' (cons V : identity f) V
   | getIdentity3 = {f}{V:f} (getIdent' : identity f -> f -> prop) (cons V) V