Lean 语言参考

17. `mvcgen`策略🔗

Tutorials

使用 mvcgen 验证命令式程序

mvcgen策略实现monadic 验证条件生成器：它将涉及使用 Lean 的命令式 Lean.Parser.Term.do : termdo 表示法编写的程序的目标分解为多个足以证明该目标的较小的 验证条件 (VCs)。除了描述 mvcgen 使用的参考之外，本章还包括可以独立于参考阅读的教程。

为了使用 mvcgen策略，必须导入 Std.Tactic.Do 并且必须打开命名空间 Std.Do。