grind
mvcgen
do
使用 mvcgen 验证命令式程序
mvcgen 策略实现了一个单子验证条件生成器： 它将涉及以 Lean 命令式 Lean.Parser.Term.do : termdo 记法编写的程序的目标，分解成若干更小的、足以证明原目标的验证条件（VC）。 除介绍 mvcgen 用法的参考资料外，本章还包含一篇可独立阅读的教程。
Lean.Parser.Term.do : term
要使用 mvcgen 策略，必须导入 Std.Tactic.Do 并打开命名空间 Std.Do。
Std.Tactic.Do
Std.Do
