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