Experimental monad constructs for the Lean 4 theorem prover.
- Monads built using the W-type (Free/Freer)
- Algebraic effects based on the haskell freer-simple library (Eff, EffIx)
- Freer monads and sum types built using Lean macros
- Logic monads: the Hoare Logic monad and the Dijkstra monad