维护状态🔗

由于 Lean 是纯函数式编程语言，它没有传统意义上的可变状态。不过，我们可以在不同层面用多种方式维护状态。状态单子（State Monad） 在程序执行期间维护状态，状态可以在函数调用之间传递。可变变量（Mutable variables） 让我们在同一会话的多条命令之间维护状态。最后，通过 环境扩展（Environment extensions），状态还能跨文件、跨会话持久保存。本章给出用这些不同技术维护状态的配方。

配方：

1. 状态单子：记住计算结果
2. 跨命令的可变变量
3. 可变变量：示例
4. 环境扩展与属性
5. 环境扩展与属性：示例