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