MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "DescendAscend2.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  plus : Nat -> Nat -> Nat
{}
term  f : Nat -> Nat -> Nat
term  g : Nat -> Nat -> Nat
{ f (Nat.succ n) m = f n (Nat.succ m)
; f (Nat.succ (Nat.succ (Nat.succ n))) m = plus m (g n n)
}
{ g (Nat.succ n) m = plus (g n (Nat.succ m)) (f m n)
}
error during typechecking:
Termination check for mutual block [f,g] fails for [g]