5. Monads and do-Notation
Planned Content
This chapter will describe do-notation in Lean:
-
Overview of monads
-
Desugaring of
doand its associated control structures -
Comprehensive description of the syntax of
do-notation -
Definition of being in the "same
do-block" -
Various common kinds of monads, including reader monads, state monads, and exception monads.
Tracked at issue #102