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" ---