cap-1.0: examples/allOdd.cap

main = allOdd id (Leaf Zero)

allOdd f (Leaf n) = f (odd n)
allOdd f (Branch l r) = allOdd ((flip (and)) (allOdd f r)) l

id x = x

flip f x y = f y x

and True True = True
and True False = False
and False x = False

odd x = eq (mod x (Succ (Succ Zero))) Zero

if True x y = x
if False x y = y

mod x y = if (lt x y) x (mod (sub x y) y)

sub (Succ x) (Succ y) = sub x y
sub x Zero = x

lt Zero Zero = False
lt Zero (Succ x) = True
lt (Succ x) (Succ y) = lt x y
lt (Succ x) Zero = False

lteq Zero Zero = True
lteq Zero (Succ x) = True
lteq (Succ x) (Succ y) = lteq x y
lteq (Succ x) Zero = False

eq Zero Zero = True
eq (Succ x) (Succ y) = eq x y
eq Zero (Succ y) = False
eq (Succ x) Zero = False