SubtermTermination.agda

-- Check that the termination checker can handle recursive
-- calls on subterms which aren't simply variables.
module SubtermTermination where

data N : Set where
  zero : N
  suc  : N → N

f : N → N
f (suc zero) = f zero
f _          = zero

data One? : N → Set where
  one : One? (suc zero)
  other : ∀ {n} → One? n

-- Should work for dot patterns as well
f′ : (n : N) → One? n → N
f′ (suc .zero) one = f′ zero other
f′ _           _   = zero

f″ : (n : N) → One? n → N
f″ ._ one = f″ zero other
f″ _  _   = zero

data D : Set where
  c₁ : D
  c₂ : D → D
  c₃ : D → D → D

g : D → D
g (c₃ (c₂ x) y) = g (c₂ x)
g _ = c₁

{- Andreas, 2011-07-07 subterm is not complete
   does not work with postulates or definitions

postulate
  i : {A : Set} → A → A

data NAT : N → Set where
  Zero : NAT zero
  Suc  : ∀ n → NAT (i n) → NAT (suc (i n))

h : (n : N) -> NAT n -> Set
h .zero Zero = N
h .(suc (i n)) (Suc n m) = h (i n) (i m)
-}