caledon-2.0.0.0: examples/evenodd.ncc
defn nat : prop | z = nat | s = nat -> nat defn odd : nat -> prop | odd/one = odd (s z) | odd/n = [A] even A -> odd (s A) defn even : nat -> prop | even/zero = even z | even/succ = [B] odd B -> even (s B)
defn nat : prop | z = nat | s = nat -> nat defn odd : nat -> prop | odd/one = odd (s z) | odd/n = [A] even A -> odd (s A) defn even : nat -> prop | even/zero = even z | even/succ = [B] odd B -> even (s B)