MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "mapStream2.ma" ---
--- scope checking ---
--- type checking ---
type  Stream : ++(A : Set) -> - Size -> Set
term  Stream.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : Stream A i) -> < Stream.cons i y1 y2 : Stream A $i >
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  map2 : .[i : Size] -> (Nat -> Nat) -> Stream Nat i -> Stream Nat i
error during typechecking:
map2
/// clause 1
/// pattern cons .$i u (cons i x xl)
/// pattern cons i x xl
/// in pattern cons i x xl, coinductive size sub pattern i must be dotted