18. The mvcgen tactic
The mvcgen tactic and its supporting libraries have been superseded by vcgen, which supports a wider variety of proofs and performs better.
New code should use vcgen, and existing code should migrate.
Please refer to the documentation for vcgen for details.
The mvcgen tactic implements a monadic verification condition generator:
It breaks down a goal involving a program written using Lean's imperative Lean.Parser.Term.do : termdo notation into a number of smaller verification conditions (VCs) that are sufficient to prove the goal.
In addition to a reference that describes the use of mvcgen, this chapter includes a tutorial that can be read independently of the reference.
In order to use the mvcgen tactic, Std.Tactic.Do must be imported and the namespace Std.Do must be opened.