agda/examples/Termination/StructuralOrder.agda

-- 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)
-}