ListT package:Agda

ListT done right, see https://www.haskell.org/haskellwiki/ListT_done_right_alternative There is also the list-t package on hackage (Nikita Volkov) but it again depends on other packages we do not use yet, so we rather implement the few bits we need afresh.

Lazy monadic computation of a list of results.

Telescope as list.

Lens to edit a Telescope as a list.

Lazy monadic conjunction of lazy monadic list, effects left-to-right

Lazy monadic disjunction of lazy monadic list, effects left-to-right

Case distinction over lazy list.

The join operation of the ListT m monad.

Consing a value to a lazy list.

Monadic cons.

Folding a lazy list, effects left-to-right.

Change from one monad to another

Boilerplate function to lift MonadReader through the ListT transformer.

Extending a monadic function to ListT.

Alternative implementation using foldListT.

The empty lazy list.

We can `run' a computation of a ListT as it is monadic itself.

Force all values in the lazy list, effects left-to-right

Singleton lazy list.

Monadic singleton.

Inverse to mapListT.