feat: add a tutorial chapter for mvcgen

.vale/styles/config/ignore/names.txt

@@ -1,13 +1,19 @@
+Bhavik
 Blott
 Bruijn
 Carneiro
 Collatz
+Himmel's
+Hoare
 Lua
 Madelaine
+Markus
 Mathlib
+Mehta
 Merkin
 Moura
 Peano
+Rish
 Selsam
 Simons
 Streicher
@@ -20,3 +26,4 @@ Nawrocki's
 Rustan
 Leino
 Leino's
+Vaishnav's

.vale/styles/config/ignore/terms.txt

@@ -98,8 +98,10 @@ letterlike
 linearization
 linearize
 linearizing
+logics
 lookup
 lookups
+lossy
 macro_rules
 matcher
 matchers
@@ -117,10 +119,12 @@ monad's
 monoid
 monomorphic
 monomorphism
+morphism
 multipattern
 multipatterns
 multiset
 multisets
+mvcgen
 namespace
 namespace's
 namespaces
@@ -139,12 +143,16 @@ polymorphic
 polymorphically
 ponens
 popcount
+postcondition
+postconditions
 postfix
+poststate
 predicative
 predicativity
 prepending
 preprocesses
 propositionally
+prestate
 quasiquotation
 quasiquotations
 quasiquote
@@ -207,6 +215,8 @@ uninstantiated
 unparenthesized
 uploader
 upvote
+VC
+VCs
 walkthrough
 workspace's
 zulip

Manual.lean

@@ -18,6 +18,7 @@ import Manual.ErrorExplanations
 import Manual.Tactics
 import Manual.Simp
 import Manual.Grind
+import Manual.VCGen
 import Manual.BasicTypes
 import Manual.BasicProps
 import Manual.NotationsMacros
@@ -99,6 +100,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but
 
 {include 0 Manual.Grind}
 
+{include 0 Manual.VCGen}
+
 {include 0 Manual.BasicProps}
 
 {include 0 Manual.BasicTypes}

Manual/BasicTypes/BitVec.lean

@@ -170,7 +170,7 @@ The resulting proofs rely only on the axiom {name}`Lean.ofReduceBool`; the exter
 
 :::example "Popcount"
 
-```imports
+```imports -show
 import Std.Tactic.BVDecide
 ```
 

Manual/BasicTypes/Maps.lean

@@ -7,7 +7,6 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Manual.Meta
-import Manual.Meta.ImportsBlock
 
 import Manual.BasicTypes.Maps.TreeSet
 import Manual.BasicTypes.Maps.TreeMap
@@ -177,7 +176,7 @@ A nested inductive type that occurs inside a map or set should be defined in thr
 
 :::example "Nested Inductive Types with `Std.HashMap`"
 
-```imports
+```imports -show
 import Std
 ```
 
@@ -310,7 +309,7 @@ These operations avoid creating a second reference to the value during modificat
 
 :::example "Modifying Values in Maps"
 
-```imports
+```imports -show
 import Std
 ```
 

Manual/BasicTypes/Option.lean

@@ -38,7 +38,7 @@ The {lean}`Option` API makes frequent use of this perspective.
 
 :::example "Options as Nullability"
 
-```imports
+```imports -show
 import Std
 ```
 
@@ -68,7 +68,7 @@ In many programming languages, it is important to remember to check for the null
 When using {name}`Option`, the type system requires these checks in the right places: {lean}`Option α` and {lean}`α` are not the same type, and converting from one to the other requires handling the case of {lean  (type := "Option α")}`none`.
 This can be done via helpers such as {name}`Option.getD`, or with pattern matching.
 
-```imports
+```imports -show
 import Std
 ```
 

Manual/Classes/DerivingHandlers.lean

@@ -97,7 +97,7 @@ Lean includes deriving handlers for the following classes:
 ::::keepEnv
 :::example "Deriving Handlers"
 
-```imports
+```imports -show
 import Lean.Elab
 ```
 

Manual/Grind/Linarith.lean

@@ -38,7 +38,7 @@ It can be disabled using the option `grind -linarith`.
 
 
 :::example "Goals Decided by `linarith`" (open := true)
-```imports
+```imports -show
 import Std
 ```
 ```lean -show
@@ -75,7 +75,7 @@ example {a b c d e : α} :
 :::
 
 :::example "Commutative Ring Goals Decided by `linarith`" (open := true)
-```imports
+```imports -show
 import Std
 ```
 ```lean -show

Manual/Interaction.lean

@@ -311,7 +311,7 @@ Lists all axioms that the constant transitively relies on. See {ref "print-axiom
 :::
 
 :::example "Printing Axioms"
-```imports
+```imports -show
 import Std.Tactic.BVDecide
 ```
 

Manual/Interaction/FormatRepr.lean

@@ -93,7 +93,7 @@ The most important {name Std.Format}`Format` operations are:
 ::::
 
 :::example "Widths and Newlines"
-```imports
+```imports -show
 import Std
 ```
 ```lean

Manual/Language/InductiveTypes/Structures.lean

@@ -163,7 +163,7 @@ Its constructor is named {name}`Palindrome.ofString`, rather than `Palindrome.mk
 :::
 
 ::: example "Modifiers on structure constructor"
-```imports
+```imports -show
 import Std
 ```
 The structure {lean}`NatStringBimap` maintains a finite bijection between natural numbers and strings.

Manual/Meta.lean

@@ -33,6 +33,8 @@ import Manual.Meta.Syntax
 import Manual.Meta.Tactics
 import Manual.Meta.SpliceContents
 import Manual.Meta.Markdown
+import Manual.Meta.Imports
+import Manual.Meta.Namespace
 
 
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets

Manual/Meta/Example.lean

@@ -6,8 +6,8 @@ Author: David Thrane Christiansen
 
 import VersoManual
 import Manual.Meta.Figure
+import Manual.Meta.Imports
 import Manual.Meta.LzCompress
-import Manual.Meta.ImportsBlock
 import Lean.Elab.InfoTree.Types
 
 open Verso Doc Elab

Manual/Meta/Imports.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+import Lean.Elab.InfoTree.Types
+import SubVerso.Highlighting.Code
+
+open scoped Lean.Doc.Syntax
+
+open Verso Doc Elab
+open Lean Elab
+open Verso.Genre.Manual InlineLean Scopes
+open Verso.SyntaxUtils
+open SubVerso.Highlighting
+open ArgParse
+
+namespace Manual
+
+structure ImportsParams where
+  «show» : Bool := true
+
+instance : FromArgs ImportsParams m where
+  fromArgs := ImportsParams.mk <$> .flag `show true (some "Whether to show the import header")
+
+@[code_block]
+def imports : CodeBlockExpanderOf ImportsParams
+  | { «show» } , str => do
+    let altStr ← parserInputString str
+    let p := Parser.whitespace >> Parser.Module.header.fn
+    let headerStx ← p.parseString altStr
+    let hl ← highlight headerStx #[] {}
+    if «show» then
+      ``(Block.other (Block.lean $(quote hl) {}) #[Block.code $(quote str.getString)])
+    else
+      ``(Block.empty)

Manual/Meta/Namespace.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+import Lean.Elab.InfoTree.Types
+import SubVerso.Highlighting.Code
+
+open scoped Lean.Doc.Syntax
+
+open Verso Doc Elab
+open Lean Elab
+open Verso.Genre.Manual InlineLean Scopes
+open Verso.SyntaxUtils
+open SubVerso.Highlighting
+
+@[role]
+def «namespace» : RoleExpanderOf Unit
+  | (), #[arg] => do
+    let `(inline|code($s)) := arg
+      | throwErrorAt arg "Expected code"
+    -- TODO validate that namespace exists? Or is that too strict?
+    -- TODO namespace domain for documentation
+    ``(Inline.code $(quote s.getString))
+  | _, more =>
+    if h : more.size > 0 then
+      throwErrorAt more[0] "Expected code literal with the namespace"
+    else
+      throwError "Expected code literal with the namespace"

Manual/Monads/Syntax.lean

@@ -428,6 +428,9 @@ In addition to convenient support for sequential computations with data dependen
 These effects are implemented via transformations of the entire {keywordOf Lean.Parser.Term.do}`do` block in a manner akin to {tech}[monad transformers], rather than via a local desugaring.
 
 ## Early Return
+%%%
+tag := "early-return"
+%%%
 
 Early return terminates a computation immediately with a given value.
 The value is returned from the closest containing {keywordOf Lean.Parser.Term.do}`do` block; however, this may not be the closest `do` keyword.
@@ -452,6 +455,9 @@ Internally, the {keywordOf Lean.Parser.Term.do}`do` elaborator performs a transl
 On its own, {keywordOf Lean.Parser.Term.doReturn}`return` is short for {keywordOf Lean.Parser.Term.doReturn}`return`​` `​{lean}`()`.
 
 ## Local Mutable State
+%%%
+tag := "let-mut"
+%%%
 
 Local mutable state is mutable state that cannot escape the {keywordOf Lean.Parser.Term.do}`do` block in which it is defined.
 The {keywordOf Lean.Parser.Term.doLet}`let mut` binder introduces a locally-mutable binding.

Manual/NotationsMacros.lean

@@ -620,7 +620,7 @@ The optional suffix `?` in syntax and splices correspond with each other.
 
 ::::keepEnv
 :::example "Suffixed Splices"
-```imports
+```imports -show
 import Lean.Elab
 ```
 ```lean -show
@@ -697,7 +697,7 @@ macro_rules
 
 ::::keepEnv
 :::example "Optional Splices"
-```imports
+```imports -show
 import Lean.Elab
 ```
 The following syntax declaration optionally matches a term between two tokens.

Manual/NotationsMacros/Elab.lean

@@ -91,7 +91,7 @@ A command elaborator has type {name}`CommandElab`, which is an abbreviation for
 Command elaborators may be implicitly defined using {keywordOf Lean.Parser.Command.elab_rules}`elab_rules`, or explicitly by defining a function and applying the {attr}`command_elab` attribute.
 
 :::example "Querying the Environment"
-```imports
+```imports -show
 import Lean.Elab
 ```
 ```lean -show
@@ -143,7 +143,7 @@ The optional {lean}`Expr` parameter is the type expected for the term being elab
 Like command elaborators, term elaborators may be implicitly defined using {keywordOf Lean.Parser.Command.elab_rules}`elab_rules`, or explicitly by defining a function and applying the {attr}`term_elab` attribute.
 
 :::example "Avoiding a Type"
-```imports
+```imports -show
 import Lean.Elab
 ```
 ```lean -show
@@ -205,7 +205,7 @@ Got unwanted type String
 :::
 
 :::example "Using Any Local Variable"
-```imports
+```imports -show
 import Lean.Elab
 ```
 ```lean -show