MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "scolist_not_lsc1.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : ^ Size -> Set
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[i : Size] -> ^(y1 : Nat i) -> < Nat.succ i y1 : Nat $i >
type  Colist : ^(A : Set) -> ^ Size -> Set
term  Colist.nil : .[A : Set] -> .[i : Size] -> < Colist.nil i : Colist A $i >
term  Colist.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : Colist A i) -> < Colist.cons i y1 y2 : Colist A $i >
term  length : .[i : Size] -> .[A : Set] -> Colist A i -> Nat i
error during typechecking:
checking type of length for admissibility
/// new A : _
/// new i : _
/// new i <= #
/// admType: checking (.[A : Set] -> Colist A i -> Nat i{i = v2}) admissible in v2
/// new A : Set
/// admType: checking ((Colist v3 v2)::Tm -> {Nat i {A = v3, i = v2}}) admissible in v2
/// type  Colist A i  not lower semi continuous in  i