MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "scolist_not_lsc2.ma" ---
--- scope checking ---
--- type checking ---
type  Nat : + Size -> Set
term  Nat.zero : .[s!ze : Size] -> .[i < s!ze] -> Nat s!ze
term  Nat.zero : .[i : Size] -> < Nat.zero i : Nat $i >
term  Nat.succ : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat i -> Nat s!ze
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 >
type  CoNat : ^ Size -> Set
term  CoNat.cozero : .[i : Size] -> < CoNat.cozero i : CoNat $i >
term  CoNat.cosucc : .[i : Size] -> ^(y1 : CoNat i) -> < CoNat.cosucc i y1 : CoNat $i >
term  z : CoNat #
term  z = CoNat.cozero [#]
term  length2 : .[i : Size] -> .[A : Set] -> Colist A i -> CoNat i
{ length2 [.$i] [A] (Colist.nil [i]) = CoNat.cozero [i]
; length2 [.$i] [A] (Colist.cons [i] a as) = CoNat.cosucc [i] (length2 [i] [A] as)
}
term  omega' : .[i : Size] -> CoNat i
error during typechecking:
omega'
/// clause 1
/// pattern $i
/// checkPattern $i : matching on size, checking that target .[i : Size] -> CoNat i ends in correct coinductive sized type
/// new i <= #
/// endsInSizedCo: CoNat i
/// endsInSizedCo: target CoNat i of corecursive function is neither a CoSet or codata of size i nor a tuple type