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.
(This variant allows starting with a specified
list β of elements, as well. )
mllist using a function which returns values in the (alternative) monad.
Whenever the function "succeeds", we accept the element, and reject otherwise.