MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "drop.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 >
type  Stream : - Size -> Set
term  Stream.cons : .[i : Size] -> ^(y1 : SNat #) -> ^(y2 : Stream i) -> < Stream.cons i y1 y2 : Stream $i >
term  drop : .[i : Size] -> SNat i -> .[j : Size] -> Stream j -> Stream j
error during typechecking:
drop
/// clause 2
/// right hand side
/// checkExpr 7 |- drop i y j xs : Stream $j
/// leqVal' (subtyping)  < drop [i] y [j] xs : Stream j >  <=+  Stream $j
/// leqVal' (subtyping)  Stream j  <=+  Stream $j
/// leqVal'  j  <=-  $j : Size
/// leSize j <=- $j
/// leSize' $j <= j
/// leSize: 0 + 1 <= 0 failed