MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "DescendAscendTerm.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
term  g : Nat -> Nat -> Nat
{ f (Nat.succ (Nat.succ (Nat.succ n))) = g n n
}
{ g (Nat.succ n) m = plus (g n (Nat.succ m)) (f n)
}
--- evaluating ---
--- closing "DescendAscendTerm.ma" ---