MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "CoNotLowerSemi.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) -> -(i : Size) -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(head : A) -> ^(tail : .[j < i] -> Stream A j) -> < Stream.cons head tail : Stream A i >
term  head : .[A : Set] -> .[i : Size] -> (cons : Stream A i) -> A
{ head [A] [i] (Stream.cons #head #tail) = #head
}
term  tail : .[A : Set] -> .[i : Size] -> (cons : Stream A i) -> .[j < i] -> Stream A j
{ tail [A] [i] (Stream.cons #head #tail) = #tail
}
term  repeat : .[A : Set] -> (a : A) -> .[i : Size] -> Stream A i
{ repeat [A] a [i] = Stream.cons a ([\ j ->] repeat [A] a [j])
}
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