MiniAgda by Andreas Abel and Karl Mehltretter --- opening "adm/adm1.ma" --- --- scope checking --- --- type checking --- type Nat : + Size -> Set term Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze term Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i > term Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze term Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i > term foo : .[i : Size] -> Nat i {} type foo2 : (i : Size) -> Nat $i -> Set { foo2 i (Nat.zero [.i]) = foo2 i (Nat.zero [i]) ; foo2 i (Nat.succ [.i] x) = Nat # } error during typechecking: Termination check for function foo2 fails