doc: port mvcgen documentation to vcgen and Std.WP - #927

Draft

sgraf812 wants to merge 17 commits into

nightly-testingfrom

vcgen-docs-nightly

Commits on Aug 20, 2026

doc: copy mvcgen chapter and tutorial as a base for vcgen docs
sgraf812
committed
2f4f11d
doc: disambiguate the copied vcgen chapter and tutorial
sgraf812
committed
f417558
doc: port tutorial intro and loop sections to vcgen
sgraf812
committed
5c90431
doc: port tutorial control flow section to vcgen
sgraf812
committed
0d36144
doc: port tutorial Hoare triple sections to vcgen
sgraf812
committed
45b66ee
doc: port tutorial monad transformer section to vcgen
sgraf812
committed
6906894
doc: port tutorial exceptions section to vcgen
sgraf812
committed
70fc36f
doc: port tutorial custom monad section to vcgen
sgraf812
committed
937709c
doc: replace tutorial proof mode section for vcgen
sgraf812
committed
a46a975
doc: port the manual vcgen chapter to Std.WP
sgraf812
committed
a2436f4
doc: add vcgen to the tactic reference
sgraf812
committed
c887158

Commits on Aug 21, 2026

doc: define the Identity interpretation as an instance_reducible def
sgraf812
committed
9c41e3e
doc: note the temporary Lean.Order dependency
sgraf812
committed
23ac6a6
doc: move the deftech key prefixes to the mvcgen documents
sgraf812
committed
dacfec5
doc: finish a pass over the manual entry for VCGen
sgraf812
committed
b547b93
chore: bump toolchain to nightly-2026-08-21
sgraf812
committed
7debb23
doc: port the vcgen documents to exception stacks
sgraf812
committed
1f725b7