agda/examples/Termination/TerminationTwoConstructors.agda

{-# OPTIONS --termination-depth=2 #-}

module TerminationTwoConstructors where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

f : Nat -> Nat
f zero = zero
f (suc zero) = zero
f (suc (suc n)) with zero
... | m = f (suc n)

{- this type checks with --termination-depth >= 2
calls:

 f -> f_with (-2)
 f_with -> f (+1)

-}