5. Monads and do-Notation
Planned Content
This chapter will describe do-notation in Lean:
-
Desugaring of
doand its associated control structures -
Comprehensive description of the syntax of
do-notation -
Definition of being in the "same
do-block"
Tracked at issue #102