MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "CoNotLowerSemi1.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : +(i : Size) -> Set
term  Nat.zero : .[i : Size] -> < Nat.zero : Nat i >
term  Nat.suc : .[i : Size] -> ^(jn : .[j < i] & Nat j) -> < Nat.suc jn : Nat i >
type  Stream : ++(A : Set) -> Set
term  Stream.cons : .[A : Set] -> ^(head : A) -> ^(tail : Stream A) -> < Stream.cons head tail : Stream A >
term  head : .[A : Set] -> (cons : Stream A) -> A
{ head [A] (Stream.cons #head #tail) = #head
}
term  tail : .[A : Set] -> (cons : Stream A) -> Stream A
{ tail [A] (Stream.cons #head #tail) = #tail
}
error during typechecking:
lsc
/// new s : (Stream (Nat #))
/// checkExpr 1 |- (# , s) : .[j < #] & Stream (Nat j)
/// checkForced fromList [(s,0)] |- (# , s) : .[j < #] & Stream (Nat j)
/// checkExpr 1 |- # : < #
/// leqVal' (subtyping)  < # : Size >  <=+  < #
/// leSize # <+ #
/// leSize: # < # failed