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