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