-- some examples for structural order in the termination checker module StructuralOrder where data Nat : Set where zero : Nat succ : Nat -> Nat -- c t > t for any term t -- e.g., succ (succ y) > succ y plus : Nat -> Nat -> Nat plus x (succ (succ y)) = succ (plus x (succ y)) plus x (succ zero) = succ x plus x zero = x -- constructor names do not matter -- c (c' t) > c'' t -- e.g. c0 (c1 x) > c0 x -- c0 (c0 x) > c1 x -- Actually constructor names does matter until the non-mattering is -- implemented properly. {- TEMPORARILY REMOVED by Ulf since there are problems with the constructor-name ignoring data Bin : Set where eps : Bin c0 : Bin -> Bin c1 : Bin -> Bin foo : Bin -> Nat foo eps = zero foo (c0 eps) = zero foo (c0 (c1 x)) = succ (foo (c0 x)) foo (c0 (c0 x)) = succ (foo (c1 x)) foo (c1 x) = succ (foo x) -}