MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "mapStream.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 >
term  map : .[A : Set] -> .[B : Set] -> .[i : Size] -> (A -> B) -> Stream A i -> Stream B i
{ map [A] [B] $[i < #] f (Stream.cons [.i] x xl) = Stream.cons [i] (f x) (map [A] [B] [i] f xl)
}
--- evaluating ---
--- closing "mapStream.ma" ---