Monadic lazy lists. #
An alternative construction of lazy lists (see also
with "lazyness" controlled by an arbitrary monad.
The inductive construction is not allowed outside of meta (indeed, we can build infinite objects).
This isn't so bad, as the typical use is with the tactic monad, in any case.
As we're in meta anyway, we don't bother with proofs about these constructions.