2
module StructuralOrder where
8
plus : Nat -> Nat -> Nat
9
plus x (succ (succ y)) = succ (plus x (succ y))
10
plus x (succ zero) = succ x
15
{- TEMPORARILY REMOVED by Ulf since there are problems with the constructor-name ignoring
24
foo (c0 (c1 x)) = succ (foo (c0 x))
25
foo (c0 (c0 x)) = succ (foo (c1 x))
26
foo (c1 x) = succ (foo x)