MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "rank2SizeQuantStream.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  Unit : Set
term  Unit.triv : < Unit.triv : Unit >
term  bla : .[i : Size] -> (.[j : Size] -> Stream Unit j -> Stream Unit j) -> Stream Unit i
{ bla $[i < #] f = f [$i] (Stream.cons [i] Unit.triv (bla [i] f))
}
--- evaluating ---
--- closing "rank2SizeQuantStream.ma" ---