. . . . . . 20 4 Monads 23 4.1 The option monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.2 The list monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 4.3 The state monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.4 The IO monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 5 Writing Tactics 31 5.1 A First Look at the Tactic Monad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.2 Names and Expressions .

and Tactic Combinators . . . . . . . . . . . . . . . . . . . . . . . 110 7.2 The Metaprogramming Monad . . . . . . . . . . . . . . . . . . . . . . . 113 7.3 Names, Expressions, Declarations, and Environments side efects, exceptions, nondetermin- ism, and other efects. The underlying abstraction is called monad. Monads generalize programs with side efects. They are popular in Haskell to write imperative programs Operations and Three Laws The option type constructor is an example of a monad, called the option monad. In general, a monad is a unary type constructor m : Type → Type that depends on some type parameter

inference can be used to infer monads associated with specific types. Lean knows about the option monad: open list def foo (l1 l2 l3 : list N) : option (list N) := do v10 ← nth l1 0, v20 ← nth l2 0, on the last line and returns it wrapped with the some constructor. Lean also knows about the list monad: open list def foo : list string := do n ← range 10, a ← ["a", "b", "c", "d", "e", "f", "g", "h" results are concatenated into a single list. The standard library also defines a state monad, and a special tactic monad provides metaprogramming access to an internal tactic state, allowing users to write