QingLong (青龙)

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)
• Free and Freer monads built using Lean macros
• Logic monads: the Hoare Logic monad and the Dijkstra monad