MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "InvalidSizeP.ma" ---
--- scope checking ---
--- type checking ---
type  SNat : + Size -> Set
term  SNat.zero : .[s!ze : Size] -> .[i < s!ze] -> SNat s!ze
term  SNat.zero : .[i : Size] -> < SNat.zero i : SNat $i >
term  SNat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ SNat i -> SNat s!ze
term  SNat.succ : .[i : Size] -> ^(y1 : SNat i) -> < SNat.succ i y1 : SNat $i >
term  test : .[i : Size] -> SNat i -> SNat i -> SNat i
error during typechecking:
test
/// clause 1
/// pattern succ (l < k) y
/// pattern l < k
/// new l < v0
/// adding size rel. v3 + 1 <= v0
/// adding size rel. v3 + 1 <= v1
/// leqVal' (subtyping)  < i  <=+  < k
/// leSize i <=+ k
/// leSize' i <= k
/// bound not entailed