Maintaining State🔗

Since Lean is a pure functional programming language, it does not have mutable state in the traditional sense. However, we can maintain state in various ways at various levels. State Monads maintain state during execution of a program, and the state can be passed during function calls. Mutable variables allow us to maintain state across commands in the same session. Finally, state can be persisted across files and sessions by using Environment extensions. In this chapter we give recipes for maintaining state using these different techniques.

Recipes:

1. State Monad: Remembering Computations
2. Mutable Variables across commands
3. Mutable Variables: Example
4. Environment Extensions and Attributes
5. Environment Extensions and Attributes: Example