Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Branch: master
Fetching contributors…

Cannot retrieve contributors at this time

9 lines (8 sloc) 0.572 kB
Thanks to Arthur Charguéraud <> and Roberto di Cosmo
<> for their helpful comments on specifying lazily
evaluated datastructures. They have used the automated theorem prover
"Coq" to prove many of Okasaki's datastructures correct, including their
computational complexity. An earlier implementation of streams in this
library differed slightly from theirs, and it was not clear whether this
could break their complexity guarantees. The new representation is based
on Arthur's and Rboerto's recommendations and should be sound.
Jump to Line
Something went wrong with that request. Please try again.