Library Coq.Lists.StreamMemo
Memoization
Successive outputs of a given function
f are stored in
a stream in order to avoid duplicated computations.
Building with possible sharing using a iterator g :
We now suppose in addition that f n is in fact the n-th
iterate of a function g.
For a dependent function, the previous solution is
reused thanks to a temporary hiding of the dependency
in a "container" memo_val.
Finally, a version with both dependency and iterator
An example with the memo function on factorial