caledon-2.0.0.0: examples/test.ncc

defn num  : prop
   | zero = num
   | succ = num → num

defn add   : num → num → num → prop
   | add-z = [N] add zero N N
   | add-s = [N][M][R] add N M R → add (succ N) M (succ R)

query sum-1 = exists v . add (succ zero) (succ zero) v
-- query sum-2 = exists v . add (succ zero) v (succ (succ (succ zero)))
-- query sum-3 = exists v . add zero (succ zero) v