5.ย Monads and do-Notation๐Ÿ”—

Planned Content

This chapter will describe do-notation in Lean:

  • Overview of monads

  • 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