experiment: index recursor_rules by constructor index

This PR adds and expands `grind` related docstrings.

src/Init/Data/Iterators/Combinators/Monadic/ULift.lean

@@ -19,6 +19,7 @@ universe v u v' u'
 section ULiftT
 
 /-- `ULiftT.{v, u}` shrinks a monad on `Type max u v` to a monad on `Type u`. -/
+@[expose]  -- for codegen
 def ULiftT (n : Type max u v → Type v') (α : Type u) := n (ULift.{v} α)
 
 /-- Returns the underlying `n`-monadic representation of a `ULiftT n α` value. -/

src/Init/Data/Slice/Array/Iterator.lean

@@ -10,7 +10,7 @@ public import Init.Core
 public import Init.Data.Slice.Array.Basic
 import Init.Data.Iterators.Combinators.Attach
 import Init.Data.Iterators.Combinators.FilterMap
-import Init.Data.Iterators.Combinators.ULift
+public import Init.Data.Iterators.Combinators.ULift
 public import Init.Data.Iterators.Consumers.Collect
 public import Init.Data.Iterators.Consumers.Loop
 public import Init.Data.Range.Polymorphic.Basic
@@ -31,7 +31,6 @@ open Std Slice PRange Iterators
 
 variable {shape : RangeShape} {α : Type u}
 
-@[no_expose]
 instance {s : Subarray α} : ToIterator s Id α :=
   .of _
     (PRange.Internal.iter (s.internalRepresentation.start...<s.internalRepresentation.stop)

src/Init/Grind/Attr.lean

@@ -129,6 +129,14 @@ If `grind!` is used, then only minimal indexable subexpressions are considered.
 -/
 syntax grindLR     := patternIgnore("⇒" <|> "=>")
 /--
+The `.` modifier instructs `grind` to select a multi-pattern by traversing the conclusion of the
+theorem, and then the hypotheses from eft to right. We say this is the default modifier.
+Each time it encounters a subexpression which covers an argument which was not
+previously covered, it adds that subexpression as a pattern, until all arguments have been covered.
+If `grind!` is used, then only minimal indexable subexpressions are considered.
+-/
+syntax grindDef    := patternIgnore("." <|> "·") (grindGen)?
+/--
 The `usr` modifier indicates that this theorem was applied using a
 **user-defined instantiation pattern**. Such patterns are declared with
 the `grind_pattern` command, which lets you specify how `grind` should
@@ -206,9 +214,48 @@ syntax grindMod :=
     grindEqBoth <|> grindEqRhs <|> grindEq <|> grindEqBwd <|> grindBwd
     <|> grindFwd <|> grindRL <|> grindLR <|> grindUsr <|> grindCasesEager
     <|> grindCases <|> grindIntro <|> grindExt <|> grindGen <|> grindSym <|> grindInj
+    <|> grindDef
+
+/--
+Marks a theorem or definition for use by the `grind` tactic.
+
+An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
+controls how `grind` uses the declaration:
+* whether it is applied forwards, backwards, or both,
+* whether equalities are used on the left, right, or both sides,
+* whether case-splits, constructors, extensionality, or injectivity are applied,
+* or whether custom instantiation patterns are used.
+
+See the individual modifier docstrings for details.
+-/
 syntax (name := grind) "grind" (ppSpace grindMod)? : attr
+/--
+Like `@[grind]`, but enforces the **minimal indexable subexpression condition**:
+when several subterms cover the same free variables, `grind!` chooses the smallest one.
+
+This influences E-matching pattern selection.
+
+### Example
+```lean
+theorem fg_eq (h : x > 0) : f (g x) = x
+
+@[grind <-] theorem fg_eq (h : x > 0) : f (g x) = x
+-- Pattern selected: `f (g x)`
+
+-- With minimal subexpression:
+@[grind! <-] theorem fg_eq (h : x > 0) : f (g x) = x
+-- Pattern selected: `g x`
+-/
 syntax (name := grind!) "grind!" (ppSpace grindMod)? : attr
+/--
+Like `@[grind]`, but also prints the pattern(s) selected by `grind`
+as info messages. Useful for debugging annotations and modifiers.
+-/
 syntax (name := grind?) "grind?" (ppSpace grindMod)? : attr
+/--
+Like `@[grind!]`, but also prints the pattern(s) selected by `grind`
+as info messages. Combines minimal subexpression selection with debugging output.
+-/
 syntax (name := grind!?) "grind!?" (ppSpace grindMod)? : attr
 end Attr
 end Lean.Parser

src/Init/Grind/Injective.lean

@@ -7,7 +7,7 @@ module
 prelude
 public import Init.Data.Function
 public import Init.Classical
-
+public section
 namespace Lean.Grind
 open Function
 
@@ -31,4 +31,11 @@ noncomputable def leftInv {α : Sort u} {β : Sort v} (f : α → β) (hf : Inje
 theorem leftInv_eq {α : Sort u} {β : Sort v} (f : α → β) (hf : Injective f) [Nonempty α] (a : α) : leftInv f hf (f a) = a :=
   Classical.choose_spec (hf.leftInverse f) a
 
+@[app_unexpander leftInv]
+meta def leftInvUnexpander : PrettyPrinter.Unexpander := fun stx => do
+  match stx with
+  | `($_ $f:term $_) => `($f⁻¹)
+  | `($_ $f:term $_ $a:term) => `($f⁻¹ $a)
+  | _ => throw ()
+
 end Lean.Grind

src/Init/Grind/Norm.lean

@@ -182,7 +182,7 @@ init_grind_norm
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
   Nat.div_zero Nat.mod_zero Nat.div_one Nat.mod_one
   Nat.sub_sub Nat.pow_zero Nat.pow_one Nat.sub_self
-  Nat.one_pow Nat.zero_sub
+  Nat.one_pow Nat.zero_sub Nat.sub_zero
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_neg

src/Init/Grind/Tactics.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Attr
 public import Init.Core
-
 public section
 
 namespace Lean.Grind
@@ -98,8 +96,16 @@ structure Config where
   zeta := true
   /--
   When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
+  This solver also support commutative semirings, fields, and normalizer non-commutative rings and
+  semirings.
   -/
   ring := true
+  /--
+  Maximum number of steps performed by the `ring` solver.
+  A step is counted whenever one polynomial is used to simplify another.
+  For example, given `x^2 + 1` and `x^2 * y^3 + x * y`, the first can be
+  used to simplify the second to `-1 * y^3 + x * y`.
+  -/
   ringSteps := 10000
   /--
   When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
@@ -114,6 +120,12 @@ structure Config where
   When `true` (default: `true`), uses procedure for handling associative (and commutative) operators.
   -/
   ac := true
+  /--
+  Maximum number of steps performed by the `ac` solver.
+  A step is counted whenever one AC equation is used to simplify another.
+  For example, given `ma x z = w` and `max x (max y z) = x`, the first can be
+  used to simplify the second to `max w y = x`.
+  -/
   acSteps := 1000
   /--
   Maximum exponent eagerly evaluated while computing bounds for `ToInt` and
@@ -124,6 +136,14 @@ structure Config where
   When `true` (default: `true`), automatically creates an auxiliary theorem to store the proof.
   -/
   abstractProof := true
+  /--
+  When `true` (default: `true`), enables the procedure for handling injective functions.
+  In this mode, `grind` takes into account theorems such as:
+  ```
+  @[grind inj] theorem double_inj : Function.Injective double
+  ```
+  -/
+  inj := true
   deriving Inhabited, BEq
 
 /--
@@ -182,7 +202,10 @@ namespace Lean.Parser.Tactic
 
 syntax grindErase    := "-" ident
 syntax grindLemma    := ppGroup((Attr.grindMod ppSpace)? ident)
--- `!` for enabling minimal indexable subexpression restriction
+/--
+The `!` modifier instructs `grind` to consider only minimal indexable subexpressions
+when selecting patterns.
+-/
 syntax grindLemmaMin := ppGroup("!" (Attr.grindMod ppSpace)? ident)
 syntax grindParam    := grindErase <|> grindLemma <|> grindLemmaMin
 

src/Init/Notation.lean

@@ -855,7 +855,7 @@ which would include `#guard_msgs` itself, and would cause duplicate and/or uncap
 The top-level command elaborator only runs the linters if `#guard_msgs` is not present.
 -/
 syntax (name := guardMsgsCmd)
-  (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
+  (plainDocComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
 
 /--
 Format and print the info trees for a given command.

src/Init/System/Promise.lean

@@ -16,10 +16,6 @@ namespace IO
 
 private opaque PromisePointed : NonemptyType.{0}
 
-private structure PromiseImpl (α : Type) : Type where
-  prom : PromisePointed.type
-  h    : Nonempty α
-
 /--
 `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`.
 
@@ -33,7 +29,9 @@ Typical usage is as follows:
 If the promise is dropped without ever being resolved, `promise.result?.get` will return `none`.
 See `Promise.result!/resultD` for other ways to handle this case.
 -/
-def Promise (α : Type) : Type := PromiseImpl α
+structure Promise (α : Type) : Type where
+  private prom : PromisePointed.type
+  private h    : Nonempty α
 
 instance [s : Nonempty α] : Nonempty (Promise α) :=
   by exact Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }

src/Lean/Compiler/LCNF/Types.lean

@@ -123,27 +123,49 @@ open Meta in
 Convert a Lean type into a LCNF type used by the code generator.
 -/
 partial def toLCNFType (type : Expr) : MetaM Expr := do
-  if ← isProp type then
-    return erasedExpr
-  let type ← whnfEta type
-  match type with
-  | .sort u     => return .sort u
-  | .const ..   => visitApp type #[]
-  | .lam n d b bi =>
-    withLocalDecl n bi d fun x => do
-      let d ← toLCNFType d
-      let b ← toLCNFType (b.instantiate1 x)
-      if b.isErased then
-        return b
-      else
-        return Expr.lam n d (b.abstract #[x]) bi
-  | .forallE .. => visitForall type #[]
-  | .app ..  => type.withApp visitApp
-  | .fvar .. => visitApp type #[]
-  | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
-    return mkConst ``lcRealWorld
-  | _        => return mkConst ``lcAny
+  let res ← go type
+  if (← getEnv).header.isModule then
+    -- Under the module system, `type` may reduce differently in different modules, leading to
+    -- IR-level mismatches and thus undefined behavior. We want to make this part independent of the
+    -- current module and its view of the environment but until then, we force the user to make
+    -- involved type definitions exposed by checking whether we would infer a different type in the
+    -- public scope. We ignore failed inference in the public scope because it can easily fail when
+    -- compiling private declarations using private types, and even if that private code should
+    -- escape into different modules, it can only generate a static error there, not a
+    -- miscompilation.
+    -- Note that always using `withExporting` would not always be correct either because it is
+    -- ignored in non-`module`s and thus mismatches with upstream `module`s may again occur.
+    let res'? ← observing <| withExporting <| go type
+    if let .ok res' := res'? then
+      if res != res' then
+        throwError "Compilation failed, locally inferred compilation type{indentD res}\n\
+          differs from type{indentD res'}\n\
+          that would be inferred in other modules. This usually means that a type `def` involved \
+          with the mentioned declarations needs to be `@[expose]`d. This is a current compiler \
+          limitation for `module`s that may be lifted in the future."
+  return res
 where
+  go type := do
+    if ← isProp type then
+      return erasedExpr
+    let type ← whnfEta type
+    match type with
+    | .sort u     => return .sort u
+    | .const ..   => visitApp type #[]
+    | .lam n d b bi =>
+      withLocalDecl n bi d fun x => do
+        let d ← go d
+        let b ← go (b.instantiate1 x)
+        if b.isErased then
+          return b
+        else
+          return Expr.lam n d (b.abstract #[x]) bi
+    | .forallE .. => visitForall type #[]
+    | .app ..  => type.withApp visitApp
+    | .fvar .. => visitApp type #[]
+    | .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
+      return mkConst ``lcRealWorld
+    | _        => return mkConst ``lcAny
   whnfEta (type : Expr) : MetaM Expr := do
     let type ← whnf type
     let type' := type.eta
@@ -158,12 +180,12 @@ where
       let d := d.instantiateRev xs
       withLocalDecl n bi d fun x => do
         let isBorrowed := isMarkedBorrowed d
-        let mut d := (← toLCNFType d).abstract xs
+        let mut d := (← go d).abstract xs
         if isBorrowed then
           d := markBorrowed d
         return .forallE n d (← visitForall b (xs.push x)) bi
     | _ =>
-      let e ← toLCNFType (e.instantiateRev xs)
+      let e ← go (e.instantiateRev xs)
       return e.abstract xs
 
   visitApp (f : Expr) (args : Array Expr) := do
@@ -178,7 +200,7 @@ where
       if ← isProp arg <||> isPropFormer arg then
         result := mkApp result erasedExpr
       else if ← isTypeFormer arg then
-        result := mkApp result (← toLCNFType arg)
+        result := mkApp result (← go arg)
       else
         result := mkApp result (mkConst ``lcAny)
     return result

src/Lean/Declaration.lean

@@ -357,8 +357,8 @@ structure RecursorVal extends ConstantVal where
   numMotives : Nat
   /-- Number of minor premises -/
   numMinors : Nat
-  /-- A reduction for each Constructor -/
-  rules : List RecursorRule
+  /-- A reduction for each Constructor, indexed by constructor -/
+  rules : Array RecursorRule
   /-- It supports K-like reduction.
   A recursor is said to support K-like reduction if one can assume it behaves
   like `Eq` under axiom `K` --- that is, it has one constructor, the constructor has 0 arguments,
@@ -374,7 +374,7 @@ structure RecursorVal extends ConstantVal where
 
 @[export lean_mk_recursor_val]
 def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat)
-    (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
+    (rules : Array RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
   name, levelParams, type, all, numParams, numIndices,
   numMotives, numMinors, rules, k, isUnsafe
 }

src/Lean/DocString/Add.lean

@@ -50,23 +50,20 @@ def validateDocComment
     else
       logError err
 
-
-open Lean.Doc in
-open Parser in
+open Lean.Parser Command in
 /--
-Adds a Verso docstring to the specified declaration, which should already be present in the
-environment.
-
-`binders` should be the syntax of the parameters to the constant that is being documented, as a null
-node that contains a sequence of bracketed binders. It is used to allow interactive features such as
-document highlights and “find references” to work for documented parameters. If no parameter binders
-are available, pass `Syntax.missing` or an empty null node.
+Parses a docstring as Verso, returning the syntax if successful.
 
+When not successful, parser errors are logged.
 -/
-def versoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
-    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
-
+def parseVersoDocString
+    [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
+    [MonadResolveName m]
+    (docComment : TSyntax [``docComment, ``moduleDoc]) : m (Option Syntax) := do
+  if docComment.raw.getKind == ``docComment then
+    match docComment.raw[0] with
+    | docStx@(.node _ ``versoCommentBody _) => return docStx[1]?
+    | _ => pure ()
   let text ← getFileMap
   -- TODO fallback to string version without nice interactivity
   let some startPos := docComment.raw[1].getPos? (canonicalOnly := true)
@@ -93,7 +90,7 @@ def versoDocString
   }
   let s := mkParserState text.source |>.setPos startPos
   -- TODO parse one block at a time for error recovery purposes
-  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
+  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
 
   if !s.allErrors.isEmpty then
     for (pos, _, err) in s.allErrors do
@@ -103,11 +100,42 @@ def versoDocString
         -- TODO end position
         data := err.toString
       }
-    return (#[], #[])
-  else
-    let stx := s.stxStack.back
-    let stx := stx.getArgs
-    Doc.elabBlocks (stx.map (⟨·⟩)) |>.exec declName binders
+    return none
+  return some s.stxStack.back
+
+
+
+open Lean.Doc in
+open Lean.Parser.Command in
+/--
+Elaborates a Verso docstring for the specified declaration, which should already be present in the
+environment.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders. It is used to allow interactive features such as
+document highlights and “find references” to work for documented parameters. If no parameter binders
+are available, pass `Syntax.missing` or an empty null node.
+-/
+
+def versoDocString
+    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+  if let some stx ← parseVersoDocString docComment then
+    Doc.elabBlocks (stx.getArgs.map (⟨·⟩)) |>.exec declName binders
+  else return (#[], #[])
+
+open Lean.Doc Parser in
+open Lean.Parser.Command in
+/--
+Parses and elaborates a Verso module docstring.
+-/
+def versoModDocString
+    (range : DeclarationRange) (doc : TSyntax ``document) :
+    TermElabM VersoModuleDocs.Snippet := do
+  let level := getVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
+  Doc.elabModSnippet range (doc.raw.getArgs.map (⟨·⟩)) (level.getD 0) |>.execForModule
+
+
 
 open Lean.Doc in
 open Parser in
@@ -185,6 +213,19 @@ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadErr
   modifyEnv fun env =>
     versoDocStringExt.insert env declName docs
 
+/--
+Adds an elaborated Verso module docstring to the environment.
+-/
+def addVersoModDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m]
+  (docs : VersoModuleDocs.Snippet) : m Unit := do
+  if (getMainModuleDoc (← getEnv)).isEmpty then
+    match addVersoModuleDocSnippet (← getEnv) docs with
+    | .error e => throwError "Error adding module docs: {indentD <| toMessageData e}"
+    | .ok env' => setEnv env'
+  else
+    throwError m!"Can't add Verso-format module docs because there is already Markdown-format content present."
+
+open Lean.Parser.Command in
 /--
 Adds a Verso docstring to the environment.
 
@@ -194,7 +235,7 @@ document highlights and “find references” to work for documented parameters.
 are available, pass `Syntax.missing` or an empty null node.
 -/
 def addVersoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
     TermElabM Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
@@ -278,3 +319,20 @@ def addDocString'
   match docString? with
   | some docString => addDocString declName binders docString
   | none => return ()
+
+
+open Lean.Parser.Command in
+open Lean.Doc.Parser in
+/--
+Adds a Verso docstring to the environment.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders. It is used to allow interactive features such as
+document highlights and “find references” to work for documented parameters. If no parameter binders
+are available, pass `Syntax.missing` or an empty null node.
+-/
+def addVersoModDocString
+    (range : DeclarationRange) (docComment : TSyntax ``document) :
+    TermElabM Unit := do
+  let snippet ← versoModDocString range docComment
+  addVersoModDocStringCore snippet

src/Lean/DocString/Extension.lean

@@ -12,7 +12,7 @@ public import Lean.DocString.Links
 public import Lean.MonadEnv
 public import Init.Data.String.Extra
 public import Lean.DocString.Types
-import Lean.DocString.Markdown
+public import Lean.DocString.Markdown
 
 public section
 
@@ -38,7 +38,7 @@ instance : Repr ElabInline where
       .group (.nestD ("{ name :=" ++ .line ++ repr v.name)) ++ .line ++
       .group (.nestD ("val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
 
-private instance : Doc.MarkdownInline ElabInline where
+instance : Doc.MarkdownInline ElabInline where
   -- TODO extensibility
   toMarkdown go _i content := content.forM go
 
@@ -59,7 +59,7 @@ instance : Repr ElabBlock where
 
 
 -- TODO extensible toMarkdown
-private instance : Doc.MarkdownBlock ElabInline ElabBlock where
+instance : Doc.MarkdownBlock ElabInline ElabBlock where
   toMarkdown _goI goB _b content := content.forM goB
 
 structure VersoDocString where
@@ -214,5 +214,211 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module
 
 def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
   match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
+  | Syntax.atom _ val =>
+    return val.extract 0 (val.endPos - ⟨2⟩)
+  | Syntax.node _ `Lean.Parser.Command.versoCommentBody _ =>
+    match stx.raw[1][0] with
+    | Syntax.atom _ val =>
+      return val.extract 0 (val.endPos - ⟨2⟩)
+    | _ =>
+      throwErrorAt stx "unexpected doc string{indentD stx}"
+  | _ =>
+    throwErrorAt stx "unexpected doc string{indentD stx}"
+
+
+
+/--
+A snippet of a Verso module text.
+
+A snippet consists of text followed by subsections. Because the sequence of snippets that occur in a
+source file are conceptually a single document, they have a consistent header nesting structure.
+This means that initial textual content of a snippet is a continuation of the text at the end of the
+prior snippet.
+
+The actual hierarchical structure of the document is reconstructed from the sequence of snippets.
+
+The _terminal nesting_ of a sequence of snippets is 0 if there are no sections in the sequence.
+Otherwise, it is one greater than the nesting of the last snippet's last section. The module
+docstring elaborator maintains the invariant that each snippet's first section's level is at most
+the terminal nesting of the preceding snippets, and that the level of each section within a snippet
+is at most one greater than the preceding section's level.
+-/
+structure VersoModuleDocs.Snippet where
+  /-- Text to be inserted after the prior snippet's ending text. -/
+  text : Array (Doc.Block ElabInline ElabBlock) := #[]
+  /--
+  A sequence of parts with their absolute document nesting levels and header positions.
+  None of these parts may contain sub-parts.
+  -/
+  sections : Array (Nat × DeclarationRange × Doc.Part ElabInline ElabBlock Empty) := #[]
+  /--
+  The location of the snippet in the source file.
+  -/
+  declarationRange : DeclarationRange
+deriving Inhabited, Repr
+
+namespace VersoModuleDocs.Snippet
+
+def canNestIn (level : Nat) (snippet : Snippet) : Bool :=
+  if let some s := snippet.sections[0]? then s.1 ≤ level + 1 else true
+
+def terminalNesting (snippet : Snippet) : Option Nat :=
+  if let some s := snippet.sections.back? then s.1
+  else none
+
+def addBlock (snippet : Snippet) (block : Doc.Block ElabInline ElabBlock) : Snippet :=
+  if h : snippet.sections.size = 0 then
+    { snippet with text := snippet.text.push block }
+  else
+    { snippet with
+      sections[snippet.sections.size - 1].2.2.content :=
+        snippet.sections[snippet.sections.size - 1].2.2.content.push block }
+
+def addPart (snippet : Snippet) (level : Nat) (range : DeclarationRange) (part : Doc.Part ElabInline ElabBlock Empty) : Snippet :=
+  { snippet with
+    sections := snippet.sections.push (level, range, part) }
+
+end VersoModuleDocs.Snippet
+
+open Lean Doc ToMarkdown MarkdownM in
+instance : ToMarkdown VersoModuleDocs.Snippet where
+  toMarkdown
+    | {text, sections, ..} => do
+      text.forM toMarkdown
+      endBlock
+      for (level, _, part) in sections do
+        push ("".pushn '#' (level + 1))
+        push " "
+        for i in part.title do toMarkdown i
+        endBlock
+        for b in part.content do toMarkdown b
+        endBlock
+
+structure VersoModuleDocs where
+  snippets : PersistentArray VersoModuleDocs.Snippet := {}
+  terminalNesting : Option Nat := snippets.findSomeRev? (·.terminalNesting)
+deriving Inhabited
+
+instance : Repr VersoModuleDocs where
+  reprPrec v _ :=
+    .group <| .nest 2 <|
+      "{ " ++
+      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++ .line ++
+      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++
+      " }"
+
+namespace VersoModuleDocs
+
+def isEmpty (docs : VersoModuleDocs) : Bool := docs.snippets.isEmpty
+
+def canAdd (docs : VersoModuleDocs) (snippet : Snippet) : Bool :=
+  if let some level := docs.terminalNesting then
+    snippet.canNestIn level
+  else true
+
+
+def add (docs : VersoModuleDocs) (snippet : Snippet) : Except String VersoModuleDocs := do
+  unless docs.canAdd snippet do
+    throw "Can't nest this snippet here"
+
+  return { docs with
+    snippets := docs.snippets.push snippet,
+    terminalNesting := snippet.terminalNesting
+  }
+
+def add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs :=
+  let ok :=
+    if let some level := docs.terminalNesting then
+      snippet.canNestIn level
+    else true
+  if not ok then
+    panic! "Can't nest this snippet here"
+  else
+    { docs with
+      snippets := docs.snippets.push snippet,
+      terminalNesting := snippet.terminalNesting
+    }
+
+
+private structure DocFrame where
+  content : Array (Doc.Block ElabInline ElabBlock)
+  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
+  titleString : String
+  title : Array (Doc.Inline ElabInline)
+
+private structure DocContext where
+  content : Array (Doc.Block ElabInline ElabBlock)
+  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
+  context : Array DocFrame
+
+private def DocContext.level (ctx : DocContext) : Nat := ctx.context.size
+
+private def DocContext.close (ctx : DocContext) : Except String DocContext := do
+  if h : ctx.context.size = 0 then
+    throw "Can't close a section: none are open"
+  else
+    let last := ctx.context.back
+    pure {
+      content := last.content,
+      priorParts := last.priorParts.push {
+        title := last.title,
+        titleString := last.titleString,
+        metadata := none,
+        content := ctx.content,
+        subParts := ctx.priorParts,
+      },
+      context := ctx.context.pop
+    }
+
+private partial def DocContext.closeAll (ctx : DocContext) : Except String DocContext := do
+  if ctx.context.size = 0 then
+    return ctx
+  else
+    (← ctx.close).closeAll
+
+private partial def DocContext.addPart (ctx : DocContext) (partLevel : Nat) (part : Doc.Part ElabInline ElabBlock Empty) : Except String DocContext := do
+  if partLevel > ctx.level then throw s!"Invalid nesting: expected at most {ctx.level} but got {partLevel}"
+  else if partLevel = ctx.level then pure { ctx with priorParts := ctx.priorParts.push part }
+  else
+    let ctx ← ctx.close
+    ctx.addPart partLevel part
+
+private def DocContext.addBlocks (ctx : DocContext) (blocks : Array (Doc.Block ElabInline ElabBlock)) : Except String DocContext := do
+  if ctx.priorParts.isEmpty then pure { ctx with content := ctx.content ++ blocks }
+  else throw "Can't add content after sub-parts"
+
+private def DocContext.addSnippet (ctx : DocContext) (snippet : Snippet) : Except String DocContext := do
+  let mut ctx ← ctx.addBlocks snippet.text
+  for (l, _, p) in snippet.sections do
+    ctx ← ctx.addPart l p
+  return ctx
+
+def assemble (docs : VersoModuleDocs) : Except String VersoDocString := do
+  let mut ctx : DocContext := {content := #[], priorParts := #[], context := #[]}
+  for snippet in docs.snippets do
+    ctx ← ctx.addSnippet snippet
+  ctx ← ctx.closeAll
+  return { text := ctx.content, subsections := ctx.priorParts }
+
+end VersoModuleDocs
+
+private builtin_initialize versoModuleDocExt :
+    SimplePersistentEnvExtension VersoModuleDocs.Snippet VersoModuleDocs ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.add! e
+  exportEntriesFnEx? := some fun _ _ es level =>
+    if level < .server then
+      #[]
+    else
+      es.toArray
+}
+
+
+def getVersoModuleDocs (env : Environment) : VersoModuleDocs :=
+  versoModuleDocExt.getState env
+
+def addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment :=
+  let docs := getVersoModuleDocs env
+  if docs.canAdd snippet then
+    pure <| versoModuleDocExt.addEntry env snippet
+  else throw s!"Can't add - incorrect nesting {docs.terminalNesting.map (s!"(expected at most {·})") |>.getD ""})"

src/Lean/DocString/Formatter.lean

@@ -0,0 +1,224 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+module
+prelude
+public import Lean.PrettyPrinter.Formatter
+import Lean.DocString.Syntax
+
+
+namespace Lean.Doc.Parser
+
+open Lean.PrettyPrinter Formatter
+open Lean.Syntax.MonadTraverser
+
+open Lean.Doc.Syntax
+
+def atomString : Syntax → String
+  | .node _ _ #[x] => atomString x
+  | .atom _ x => x
+  | stx => s!"NON-ATOM {stx}"
+
+def pushAtomString : Formatter := do
+  push <| atomString (← getCur)
+  goLeft
+
+def pushAtomStrLit : Formatter := do
+  push <| (Syntax.decodeStrLit (atomString (← getCur))).getD ""
+  goLeft
+
+
+def identString : Syntax → String
+  | .node _ _ #[x] => identString x
+  | .ident _ _ x _ => toString x
+  | stx => s!"NON-IDENT {stx}"
+
+def pushIdent : Formatter := do
+  push <| identString (← getCur)
+  goLeft
+
+def rep (f : Formatter) : Formatter := concat do
+  let count := (← getCur).getArgs.size
+  visitArgs do count.forM fun _ _ => do f
+
+partial def versoSyntaxToString' (stx : Syntax) : ReaderT Nat (StateM String) Unit := do
+  if stx.getKind == nullKind then
+    stx.getArgs.forM versoSyntaxToString'
+  else
+    match stx with
+    | `(arg_val|$s:str) => out <| atomString s
+    | `(arg_val|$n:num) => out <| atomString n
+    | `(arg_val|$x:ident) => out <| identString x
+    | `(doc_arg|($x := $v)) | `(doc_arg|$x:ident := $v) =>
+      out "("
+      out <| identString x
+      out " := "
+      versoSyntaxToString' v
+      out ")"
+    | `(doc_arg|+%$tk$x:ident) | `(doc_arg|-%$tk$x:ident) =>
+      out <| atomString tk
+      out <| identString x
+    | `(doc_arg|$x:arg_val) => versoSyntaxToString' x
+    | `(inline|$s:str) => out s.getString
+    | `(inline|_[%$tk1 $inl* ]%$tk2) | `(inline|*[%$tk1 $inl* ]%$tk2) =>
+      out <| atomString tk1
+      inl.forM versoSyntaxToString'
+      out <| atomString tk2
+    | `(inline|link[%$tk1 $inl* ]%$tk2 $tgt) =>
+      out <| atomString tk1
+      inl.forM versoSyntaxToString'
+      out <| atomString tk2
+      versoSyntaxToString' tgt
+    | `(inline|image(%$tk1 $alt )%$tk2 $tgt) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString alt)).getD ""
+      out <| atomString tk2
+      versoSyntaxToString' tgt
+    | `(inline|role{$name $args*}[$inls*]) =>
+      out "{"
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "}["
+      inls.forM versoSyntaxToString'
+      out "]"
+    | `(inline|code(%$tk1$s)%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+      out <| atomString tk2
+    | `(inline|footnote(%$tk1 $ref )%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
+      out <| atomString tk2
+    | `(inline|line! $s) =>
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+    | `(inline|\math%$tk1 code(%$tk2 $s )%$tk3)
+    | `(inline|\displaymath%$tk1 code(%$tk2 $s )%$tk3) =>
+      out <| atomString tk1
+      out <| atomString tk2
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+      out <| atomString tk3
+    | `(link_target|[%$tk1 $ref ]%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
+      out <| atomString tk2
+    | `(link_target|(%$tk1 $url )%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString url)).getD ""
+      out <| atomString tk2
+    | `(block|header($n){$inl*}) =>
+      out <| "#".pushn '#' n.getNat ++ " "
+      inl.forM versoSyntaxToString'
+      endBlock
+    | `(block|para[$inl*]) =>
+      startBlock
+      inl.forM versoSyntaxToString'
+      endBlock
+    | `(block|ul{$items*}) =>
+      startBlock
+      items.forM fun
+        | `(list_item|* $blks*) => do
+          out "* "
+          withReader (· + 2) (blks.forM versoSyntaxToString')
+          endBlock
+        | _ => pure ()
+      endBlock
+    | `(block|ol($n){$items*}) =>
+      startBlock
+      let mut n := n.getNat
+      for item in items do
+        match item with
+        | `(list_item|* $blks*) => do
+          out s!"{n}. "
+          withReader (· + 2) (blks.forM versoSyntaxToString')
+          endBlock
+          n := n + 1
+        | _ => pure ()
+      endBlock
+    | `(block| > $blks*) =>
+      startBlock
+      out "> "
+      withReader (· + 2) (blks.forM versoSyntaxToString')
+      endBlock
+    | `(block| ```%$tk1 $name $args* | $s ```%$tk2) =>
+      startBlock
+      out <| atomString tk1
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "\n"
+      let i ← read
+      let s := Syntax.decodeStrLit (atomString s) |>.getD ""
+        |>.split (· == '\n')
+        |>.map ("".pushn ' ' i ++ · ) |> "\n".intercalate
+      out s
+      out <| "".pushn ' ' i
+      out <| atomString tk2
+      endBlock
+    | `(block| :::%$tk1 $name $args* {$blks*}%$tk2) =>
+      startBlock
+      out <| atomString tk1
+      out " "
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "\n"
+      blks.forM versoSyntaxToString'
+      let i ← read
+      out <| "".pushn ' ' i
+      out <| atomString tk2
+      endBlock
+    | `(block|command{ $name $args* }) =>
+      startBlock
+      out <| "{"
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "}"
+      endBlock
+
+    | other => out (toString other)
+where
+  out (s : String) : ReaderT Nat (StateM String) Unit := modify (· ++ s)
+  nl : ReaderT Nat (StateM String) Unit := read >>= fun n => modify (· ++ "\n".pushn ' ' n)
+  startBlock : ReaderT Nat (StateM String) Unit := do
+    let s ← get
+    if s.endsWith "\n" then
+      let i ← read
+      out ("".pushn ' ' i)
+  endBlock : ReaderT Nat (StateM String) Unit := do
+    let s ← get
+    if s.endsWith "\n\n" then return
+    else if s.endsWith "\n" then out "\n"
+    else out "\n\n"
+
+def formatMetadata : Formatter := do
+  visitArgs do
+    pushLine
+    visitAtom .anonymous
+    pushLine
+    metadataContents.formatter
+    pushLine
+    visitAtom .anonymous
+
+def versoSyntaxToString (stx : Syntax) : String :=
+  versoSyntaxToString' stx |>.run 0 |>.run "" |>.2
+
+public def document.formatter : Formatter := concat do
+  let stx ← getCur
+  let i := stx.getArgs.size
+  visitArgs do
+    for _ in [0:i] do
+      let blk ← getCur
+      if blk.getKind == ``Doc.Syntax.metadata_block then
+        formatMetadata
+      else
+        push (versoSyntaxToString blk)
+        goLeft

src/Lean/DocString/Markdown.lean

@@ -85,11 +85,20 @@ Generates Markdown, rendering the result from the final state, without producing
 public def MarkdownM.run' (act : MarkdownM Unit) (context : Context := {}) (state : State := {}) : String :=
   act.run context state |>.2
 
-private def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
+/--
+Adds a string to the current Markdown output.
+-/
+public def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
 
-private def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
+/--
+Terminates the current block.
+-/
+public def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
 
-private def MarkdownM.indent: MarkdownM α → MarkdownM α :=
+/--
+Increases the indentation level by one.
+-/
+public def MarkdownM.indent: MarkdownM α → MarkdownM α :=
   withReader fun st => { st with linePrefix := st.linePrefix ++ "  " }
 
 /--
@@ -159,6 +168,41 @@ private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   backticks ++ str ++ backticks
 
+private partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
+where
+  go : List (Inline i) → String × Inline i
+    | [] => ("", .empty)
+    | .text s :: more =>
+      if s.all (·.isWhitespace) then
+        let (pre, post) := go more
+        (s ++ pre, post)
+      else
+        let s1 := s.takeWhile (·.isWhitespace)
+        let s2 := s.drop s1.length
+        (s1, .text s2 ++ .concat more.toArray)
+    | .concat xs :: more => go (xs.toList ++ more)
+    | here :: more => ("", here ++ .concat more.toArray)
+
+private partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
+where
+  go : List (Inline i) → Inline i × String
+    | [] => (.empty, "")
+    | .text s :: more =>
+      if s.all (·.isWhitespace) then
+        let (pre, post) := go more
+        (pre, post ++ s)
+      else
+        let s1 := s.takeRightWhile (·.isWhitespace)
+        let s2 := s.dropRight s1.length
+        (.concat more.toArray.reverse ++ .text s2, s1)
+    | .concat xs :: more => go (xs.reverse.toList ++ more)
+    | here :: more => (.concat more.toArray.reverse ++ here, "")
+
+private def trim (inline : Inline i) : (String × Inline i × String) :=
+  let (pre, more) := trimLeft inline
+  let (mid, post) := trimRight more
+  (pre, mid, post)
+
 open MarkdownM in
 private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
   | .text s =>
@@ -166,19 +210,25 @@ private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM U
   | .linebreak s => do
     push <| s.replace "\n" ("\n" ++ (← read).linePrefix )
   | .emph xs => do
+    let (pre, mid, post) := trim (.concat xs)
+    push pre
     unless (← read).inEmph do
       push "*"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      for i in xs do inlineMarkdown i
+      inlineMarkdown mid
     unless (← read).inEmph do
       push "*"
+    push post
   | .bold xs => do
+    let (pre, mid, post) := trim (.concat xs)
+    push pre
     unless (← read).inBold do
       push "**"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      for i in xs do inlineMarkdown i
+      inlineMarkdown mid
     unless (← read).inBold do
       push "**"
+    push post
   | .concat xs =>
     for i in xs do inlineMarkdown i
   | .link content url => do

src/Lean/DocString/Parser.lean

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Parser.Types
 public import Lean.DocString.Syntax
+import Lean.PrettyPrinter.Formatter
+import Lean.Parser.Term.Basic
 
 set_option linter.missingDocs true
 
@@ -231,6 +233,16 @@ public def fakeAtom (str : String) (info : SourceInfo := SourceInfo.none) : Pars
   let atom := .atom info str
   s.pushSyntax atom
 
+/--
+Construct a “fake” atom with the given string content, with zero-width source information at the
+current position.
+
+Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
+different enough from Lean's that this isn't always a good match.
+-/
+private def fakeAtomHere (str : String) : ParserFn :=
+  withInfoSyntaxFn skip.fn (fun info => fakeAtom str (info := info))
+
 private def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
@@ -586,7 +598,7 @@ A linebreak that isn't a block break (that is, there's non-space content on the
 def linebreak (ctxt : InlineCtxt) : ParserFn :=
   if ctxt.allowNewlines then
     nodeFn ``linebreak <|
-      andthenFn (withInfoSyntaxFn skip.fn (fun info => fakeAtom "line!" info)) <|
+      andthenFn (fakeAtomHere "line!") <|
         nodeFn strLitKind <|
         asStringFn (quoted := true) <|
           atomicFn (chFn '\n' >> lookaheadFn (manyFn (chFn ' ') >> notFollowedByFn (chFn '\n' <|> blockOpener) "newline"))
@@ -795,6 +807,9 @@ open Lean.Parser.Term in
 def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
+def withPercents : ParserFn → ParserFn := fun p =>
+  adaptUncacheableContextFn (fun c => {c with tokens := c.tokens.insert "%%%" "%%%"}) p
+
 open Lean.Parser.Term in
 /--
 Parses a metadata block, which contains the contents of a Lean structure initialization but is
@@ -803,8 +818,7 @@ surrounded by `%%%` on each side.
 public def metadataBlock : ParserFn :=
   nodeFn ``metadata_block <|
     opener >>
-    metadataContents.fn >>
-    takeWhileFn (·.isWhitespace) >>
+    withPercents metadataContents.fn >>
     closer
 where
   opener := atomicFn (bolThen (eatSpaces >> strFn "%%%") "%%% (at line beginning)") >> eatSpaces >> ignoreFn (chFn '\n')
@@ -956,35 +970,35 @@ mutual
     nodeFn ``ul <|
       lookaheadUnorderedListIndicator ctxt fun type =>
         withCurrentColumn fun c =>
-          fakeAtom "ul{" >>
+          fakeAtomHere "ul{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inr type⟩  :: ctxt.inLists}) >>
-          fakeAtom "}"
+          fakeAtomHere "}"
 
   /-- Parses an ordered list. -/
   public partial def orderedList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``ol <|
-      fakeAtom "ol(" >>
+      fakeAtomHere "ol(" >>
       lookaheadOrderedListIndicator ctxt fun type _start => -- TODO? Validate list numbering?
         withCurrentColumn fun c =>
-          fakeAtom ")" >> fakeAtom "{" >>
+          fakeAtomHere ")" >> fakeAtomHere "{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inl type⟩  :: ctxt.inLists}) >>
-          fakeAtom "}"
+          fakeAtomHere "}"
 
   /-- Parses a definition list. -/
   public partial def definitionList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``dl <|
       atomicFn (onlyBlockOpeners >> takeWhileFn (· == ' ') >> ignoreFn (lookaheadFn (chFn ':' >> chFn ' ')) >> guardMinColumn ctxt.minIndent) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "dl{" info) >>
+      fakeAtomHere "dl{" >>
       withCurrentColumn (fun c => many1Fn (descItem {ctxt with minIndent := c})) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" info)
+      fakeAtomHere "}"
 
   /-- Parses a paragraph (that is, a sequence of otherwise-undecorated inlines). -/
   public partial def para (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``para <|
       atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "para{" (info := info)) >>
+      fakeAtomHere "para{" >>
       textLine >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" (info := info))
+      fakeAtomHere "}"
 
   /-- Parses a header. -/
   public partial def header (ctxt : BlockCtxt) : ParserFn :=
@@ -999,7 +1013,7 @@ mutual
             fakeAtom ")") >>
       fakeAtom "{" >>
       textLine (allowNewlines := false) >>
-      fakeAtom "}"
+      fakeAtomHere "}"
 
   /--
   Parses a code block. The resulting string literal has already had the fences' leading indentation
@@ -1170,3 +1184,56 @@ mutual
   -/
   public partial def document (blockContext : BlockCtxt := {}) : ParserFn := ignoreFn (manyFn blankLine) >> blocks blockContext
 end
+
+section
+open Lean.PrettyPrinter
+
+/--
+Parses as `ifVerso` if the option `doc.verso` is `true`, or as `ifNotVerso` otherwise.
+-/
+public def ifVersoFn (ifVerso ifNotVerso : ParserFn) : ParserFn := fun c s =>
+  if c.options.getBool `doc.verso then ifVerso c s
+  else ifNotVerso c s
+
+@[inherit_doc ifVersoFn]
+public def ifVerso (ifVerso ifNotVerso : Parser) : Parser where
+  fn :=
+    ifVersoFn ifVerso.fn ifNotVerso.fn
+
+/--
+Formatter for `ifVerso`—formats according to the underlying formatters.
+-/
+@[combinator_formatter ifVerso, expose]
+public def ifVerso.formatter (f1 f2 : Formatter) : Formatter := f1 <|> f2
+
+/--
+Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthesizers.
+-/
+@[combinator_parenthesizer ifVerso, expose]
+public def ifVerso.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2
+
+/--
+Disables the option `doc.verso` while running a parser.
+-/
+public def withoutVersoSyntax (p : Parser) : Parser where
+  fn :=
+    adaptUncacheableContextFn
+      (fun c => { c with options := c.options.setBool `doc.verso false })
+      p.fn
+  info := p.info
+
+/--
+Formatter for `withoutVersoSyntax`—formats according to the underlying formatter.
+-/
+@[combinator_formatter withoutVersoSyntax, expose]
+public def withoutVersoSyntax.formatter (p : Formatter) : Formatter := p
+/--
+Parenthesizer for `withoutVersoSyntax`—parenthesizes according to the underlying parenthesizer.
+-/
+@[combinator_parenthesizer withoutVersoSyntax, expose]
+public def withoutVersoSyntax.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+
+end
+
+builtin_initialize
+  register_parser_alias withoutVersoSyntax

src/Lean/DocString/Syntax.lean

@@ -7,14 +7,8 @@ Author: David Thrane Christiansen
 module
 
 prelude
-
-import Init.Prelude
-import Init.Notation
-public import Lean.Parser.Types
-import Lean.Syntax
-import Lean.Parser.Extra
-public import Lean.Parser.Term
-meta import Lean.Parser.Term
+public import Lean.Parser.Term.Basic
+meta import Lean.Parser.Term.Basic
 
 
 /-!
@@ -63,22 +57,28 @@ scoped syntax (name:=arg_num) num : arg_val
 
 /-- Arguments -/
 declare_syntax_cat doc_arg
-/-- Anonymous positional arguments -/
+/-- Anonymous positional argument -/
+@[builtin_doc]
 scoped syntax (name:=anon) arg_val : doc_arg
-/-- Named arguments -/
+/-- Named argument -/
+@[builtin_doc]
 scoped syntax (name:=named) "(" ident " := " arg_val ")": doc_arg
-/-- Named arguments, without parentheses. -/
+@[inherit_doc named, builtin_doc]
 scoped syntax (name:=named_no_paren) ident " := " arg_val : doc_arg
-/-- Boolean flags, turned on -/
+/-- Boolean flag, turned on -/
+@[builtin_doc]
 scoped syntax (name:=flag_on) "+" ident : doc_arg
-/-- Boolean flags, turned off -/
+/-- Boolean flag, turned off -/
+@[builtin_doc]
 scoped syntax (name:=flag_off) "-" ident : doc_arg
 
 /-- Link targets, which may be URLs or named references -/
 declare_syntax_cat link_target
-/-- A reference to a URL -/
+/-- A URL target, written explicitly. Use square brackets for a named target. -/
+@[builtin_doc]
 scoped syntax (name:=url) "(" str ")" : link_target
-/-- A named reference -/
+/-- A named reference to a URL defined elsewhere. Use parentheses to write the URL here. -/
+@[builtin_doc]
 scoped syntax (name:=ref) "[" str "]" : link_target
 
 /--
@@ -91,26 +91,87 @@ This syntax uses the following conventions:
 -/
 declare_syntax_cat inline
 scoped syntax (name:=text) str : inline
-/-- Emphasis (often rendered as italics) -/
+/--
+Emphasis, often rendered as italics.
+
+Emphasis may be nested by using longer sequences of `_` for the outer delimiters. For example:
+```
+Remember: __always butter the _rugbrød_ before adding toppings!__
+```
+Here, the outer `__` is used to emphasize the instructions, while the inner `_` indicates the use of
+a non-English word.
+-/
+@[builtin_doc]
 scoped syntax (name:=emph) "_[" inline* "]" : inline
-/-- Bold emphasis   -/
+/--
+Bold emphasis.
+
+A single `*` suffices to make text bold. Using `_` for emphasis.
+
+Bold text may be nested by using longer sequences of `*` for the outer delimiters.
+-/
+@[builtin_doc]
 scoped syntax (name:=bold) "*[" inline* "]" : inline
-/-- Link -/
+/--
+A link. The link's target may either be a concrete URL (written in parentheses) or a named URL
+(written in square brackets).
+-/
+@[builtin_doc]
 scoped syntax (name:=link) "link[" inline* "]" link_target : inline
-/-- Image -/
+/--
+An image, with alternate text and a URL.
+
+The alternate text is a plain string, rather than Verso markup.
+
+The image URL may either be a concrete URL (written in parentheses) or a named URL (written in
+square brackets).
+-/
+
+@[builtin_doc]
 scoped syntax (name:=image) "image(" str ")" link_target : inline
-/-- A footnote use -/
+/--
+A footnote use site.
+
+Footnotes must be defined elsewhere using the `[^NAME]: TEXT` syntax.
+-/
+@[builtin_doc]
 scoped syntax (name:=footnote) "footnote(" str ")" : inline
-/-- Line break -/
 scoped syntax (name:=linebreak) "line!" str : inline
-/-- Literal code. If the first and last characters are space, and it contains at least one non-space
-  character, then the resulting string has a single space stripped from each end.-/
+/--
+Literal code.
+
+Code may begin with any non-zero number of backticks. It must be terminated with the same number,
+and it may not contain a sequence of backticks that is at least as long as its starting or ending
+delimiters.
+
+If the first and last characters are space, and it contains at least one non-space character, then
+the resulting string has a single space stripped from each end. Thus, ``` `` `x `` ``` represents
+``"`x"``, not ``" `x "``.
+-/
+@[builtin_doc]
 scoped syntax (name:=code) "code(" str ")" : inline
-/-- A _role_: an extension to the Verso document language in an inline position -/
+/--
+A _role_: an extension to the Verso document language in an inline position.
+
+Text is given a role using the following syntax: `{NAME ARGS*}[CONTENT]`. The `NAME` is an
+identifier that determines which role is being used, akin to a function name. Each of the `ARGS` may
+have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is a sequence of inline content. If there is only one piece of content and it has
+beginning and ending delimiters (e.g. code literals, links, or images, but not ordinary text), then
+the `[` and `]` may be omitted. In particular, `` {NAME ARGS*}`x` `` is equivalent to
+``{NAME ARGS*}[`x`]``.
+-/
+@[builtin_doc]
 scoped syntax (name:=role) "role{" ident doc_arg* "}" "[" inline* "]"  : inline
 /-- Inline mathematical notation (equivalent to LaTeX's `$` notation) -/
+@[builtin_doc]
 scoped syntax (name:=inline_math) "\\math" code : inline
 /-- Display-mode mathematical notation -/
+@[builtin_doc]
 scoped syntax (name:=display_math) "\\displaymath" code : inline
 
 /--
@@ -132,40 +193,130 @@ declare_syntax_cat block
 
 /-- Items from both ordered and unordered lists -/
 declare_syntax_cat list_item
-/-- List item -/
+/-- A list item -/
+@[builtin_doc]
 syntax (name:=li) "*" block* : list_item
 
 /-- A description of an item -/
 declare_syntax_cat desc_item
 /-- A description of an item -/
+@[builtin_doc]
 scoped syntax (name:=desc) ":" inline* "=>" block* : desc_item
 
+/-- Paragraph -/
+@[builtin_doc]
 scoped syntax (name:=para) "para[" inline+ "]" : block
 /-- Unordered List -/
+@[builtin_doc]
 scoped syntax (name:=ul) "ul{" list_item* "}" : block
-/-- Definition list -/
+/-- Description list -/
+@[builtin_doc]
 scoped syntax (name:=dl) "dl{" desc_item* "}" : block
 /-- Ordered list -/
+@[builtin_doc]
 scoped syntax (name:=ol) "ol(" num ")" "{" list_item* "}" : block
-/-- Literal code -/
+/--
+A code block that contains literal code.
+
+Code blocks have the following syntax:
+````
+```(NAME ARGS*)?
+CONTENT
+```
+````
+
+`CONTENT` is a literal string. If the `CONTENT` contains a sequence of three or more backticks, then
+the opening and closing ` ``` ` (called _fences_) should have more backticks than the longest
+sequence in `CONTENT`. Additionally, the opening and closing fences should have the same number of
+backticks.
+
+If `NAME` and `ARGS` are not provided, then the code block represents literal text. If provided, the
+`NAME` is an identifier that selects an interpretation of the block. Unlike Markdown, this name is
+not necessarily the language in which the code is written, though many custom code blocks are, in
+practice, named after the language that they contain. `NAME` is more akin to a function name. Each
+of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is interpreted according to the indentation of the fences. If the fences are indented
+`n` spaces, then `n` spaces are removed from the start of each line of `CONTENT`.
+-/
+@[builtin_doc]
 scoped syntax (name:=codeblock) "```" (ident doc_arg*)? "|" str "```" : block
-/-- Quotation -/
+/--
+A quotation, which contains a sequence of blocks that are at least as indented as the `>`.
+-/
+@[builtin_doc]
 scoped syntax (name:=blockquote) ">" block* : block
-/-- A link reference definition -/
+/--
+A named URL that can be used in links and images.
+-/
+@[builtin_doc]
 scoped syntax (name:=link_ref)  "[" str "]:" str : block
-/-- A footnote definition -/
+/--
+A footnote definition.
+-/
+@[builtin_doc]
 scoped syntax (name:=footnote_ref) "[^" str "]:" inline* : block
-/-- Custom directive -/
+/--
+A _directive_, which is an extension to the Verso language in block position.
+
+Directives have the following syntax:
+```
+:::NAME ARGS*
+CONTENT*
+:::
+```
+
+The `NAME` is an identifier that determines which directive is being used, akin to a function name.
+Each of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is a sequence of block content. Directives may be nested by using more colons in
+the outer directive. For example:
+```
+::::outer +flag (arg := 5)
+A paragraph.
+:::inner "label"
+* 1
+* 2
+:::
+::::
+```
+
+-/
+@[builtin_doc]
 scoped syntax (name:=directive) ":::" rawIdent doc_arg* "{" block:max* "}" : block
-/-- A header -/
+/--
+A header
+
+Headers must be correctly nested to form a tree structure. The first header in a document must
+start with `#`, and subsequent headers must have at most one more `#` than the preceding header.
+-/
+@[builtin_doc]
 scoped syntax (name:=header) "header(" num ")" "{" inline+ "}" : block
 
 open Lean.Parser Term in
-meta def metadataContents : Parser :=
+meta def metadataContents : Lean.Parser.Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
-/-- Metadata for this section, defined by the current genre -/
+/--
+Metadata for the preceding header.
+-/
+@[builtin_doc]
 scoped syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block
 
-/-- A block-level command -/
+/--
+A block-level command, which invokes an extension during documentation processing.
+
+The `NAME` is an identifier that determines which command is being used, akin to a function name.
+Each of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+-/
+@[builtin_doc]
 scoped syntax (name:=command) "command{" rawIdent doc_arg* "}" : block

src/Lean/DocString/Types.lean

@@ -10,6 +10,7 @@ prelude
 
 public import Init.Data.Repr
 public import Init.Data.Ord
+import Init.Data.Nat.Compare
 
 set_option linter.missingDocs true
 

src/Lean/Elab/BuiltinCommand.lean

@@ -23,13 +23,20 @@ public section
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
+  let some range ← Elab.getDeclarationRange? stx
+    | return  -- must be from partial syntax, ignore
+
   match stx[1] with
   | Syntax.atom _ val =>
-    let doc := val.extract 0 (val.endPos - ⟨2⟩)
-    let some range ← Elab.getDeclarationRange? stx
-      | return  -- must be from partial syntax, ignore
-    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+    if getVersoModuleDocs (← getEnv) |>.isEmpty then
+      let doc := val.extract 0 (val.endPos - ⟨2⟩)
+      modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+    else
+      throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."
+  | Syntax.node _ ``Lean.Parser.Command.versoCommentBody args =>
+    runTermElabM fun _ => do
+      addVersoModDocString range ⟨args.getD 0 .missing⟩
+  | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)
     (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) :

src/Lean/Elab/Deriving/Ord.lean

@@ -6,12 +6,21 @@ Authors: Dany Fabian
 module
 
 prelude
-public import Lean.Meta.Transform
-public import Lean.Elab.Deriving.Basic
-public import Lean.Elab.Deriving.Util
+public import Lean.Data.Options
+import Lean.Meta.Transform
+import Lean.Elab.Deriving.Basic
+import Lean.Elab.Deriving.Util
+import Lean.Meta.Constructions.CtorIdx
+import Lean.Meta.Constructions.CasesOnSameCtor
 import Lean.Meta.SameCtorUtils
 
-public section
+register_builtin_option deriving.ord.linear_construction_threshold : Nat := {
+  defValue := 10
+  descr := "If the inductive data type has this many or more constructors, use a different \
+    implementation for implementing `Ord` that avoids the quadratic code size produced by the \
+    default implementation.\n\n\
+    The alternative construction compiles to less efficient code in some cases, so by default \
+    it is only used for inductive types with 10 or more constructors." }
 
 namespace Lean.Elab.Deriving.Ord
 open Lean.Parser.Term
@@ -20,7 +29,7 @@ open Meta
 def mkOrdHeader (indVal : InductiveVal) : TermElabM Header := do
   mkHeader `Ord 2 indVal
 
-def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM Term := do
+def mkMatchOld (header : Header) (indVal : InductiveVal) : TermElabM Term := do
   let discrs ← mkDiscrs header indVal
   let alts ← mkAlts
   `(match $[$discrs],* with $alts:matchAlt*)
@@ -74,6 +83,59 @@ where
       alts := alts ++ (alt : Array (TSyntax ``matchAlt))
     return alts.pop.pop
 
+def mkMatchNew (header : Header) (indVal : InductiveVal) : TermElabM Term := do
+  assert! header.targetNames.size == 2
+
+  let x1 := mkIdent header.targetNames[0]!
+  let x2 := mkIdent header.targetNames[1]!
+  let ctorIdxName := mkCtorIdxName indVal.name
+  -- NB: the getMatcherInfo? assumes all mathcers are called `match_`
+  let casesOnSameCtorName ← mkFreshUserName (indVal.name ++ `match_on_same_ctor)
+  mkCasesOnSameCtor casesOnSameCtorName indVal.name
+  let alts ← Array.ofFnM (n := indVal.numCtors) fun ⟨ctorIdx, _⟩ => do
+    let ctorName := indVal.ctors[ctorIdx]!
+    let ctorInfo ← getConstInfoCtor ctorName
+    forallTelescopeReducing ctorInfo.type fun xs type => do
+      let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
+      let mut ctorArgs1 : Array Term := #[]
+      let mut ctorArgs2 : Array Term := #[]
+
+      let mut rhsCont : Term → TermElabM Term := fun rhs => pure rhs
+      for i in *...ctorInfo.numFields do
+        let x := xs[indVal.numParams + i]!
+        if occursOrInType (← getLCtx) x type then
+          -- If resulting type depends on this field, we don't need to compare
+          -- and the casesOnSameCtor only has a parameter for it once
+          ctorArgs1 := ctorArgs1.push (← `(_))
+        else
+          let userName ← x.fvarId!.getUserName
+          let a := mkIdent (← mkFreshUserName userName)
+          let b := mkIdent (← mkFreshUserName (userName.appendAfter "'"))
+          ctorArgs1 := ctorArgs1.push a
+          ctorArgs2 := ctorArgs2.push b
+          let xType ← inferType x
+          if (← isProp xType) then
+            continue
+          else
+            rhsCont := fun rhs => `(Ordering.then (compare $a $b) $rhs) >>= rhsCont
+      let rhs ← rhsCont (← `(Ordering.eq))
+      `(@fun $ctorArgs1:term* $ctorArgs2:term* =>$rhs:term)
+  if indVal.numCtors == 1 then
+    `( $(mkCIdent casesOnSameCtorName) $x1:term $x2:term rfl $alts:term* )
+  else
+    `( match h : compare ($(mkCIdent ctorIdxName) $x1:ident) ($(mkCIdent ctorIdxName) $x2:ident) with
+      | Ordering.lt => Ordering.lt
+      | Ordering.gt => Ordering.gt
+      | Ordering.eq =>
+        $(mkCIdent casesOnSameCtorName) $x1:term $x2:term (Nat.compare_eq_eq.mp h) $alts:term*
+     )
+
+def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM Term := do
+  if indVal.numCtors ≥ deriving.ord.linear_construction_threshold.get (← getOptions) then
+    mkMatchNew header indVal
+  else
+    mkMatchOld header indVal
+
 def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
   let auxFunName := ctx.auxFunNames[i]!
   let indVal     := ctx.typeInfos[i]!
@@ -105,13 +167,31 @@ private def mkOrdInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
   trace[Elab.Deriving.ord] "\n{cmds}"
   return cmds
 
+private def mkOrdEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
+  let auxFunName := ctx.auxFunNames[0]!
+  `(def $(mkIdent auxFunName):ident (x y : $(mkCIdent name)) : Ordering := compare x.ctorIdx y.ctorIdx)
+
+private def mkOrdEnumCmd (name : Name): TermElabM (Array Syntax) := do
+  let ctx ← mkContext ``Ord "ord" name
+  let cmds := #[← mkOrdEnumFun ctx name] ++ (← mkInstanceCmds ctx `Ord #[name])
+  trace[Elab.Deriving.ord] "\n{cmds}"
+  return cmds
+
 open Command
 
+def mkOrdInstance (declName : Name) : CommandElabM Unit := do
+  withoutExposeFromCtors declName do
+    let cmds ← liftTermElabM <|
+      if (← isEnumType declName) then
+        mkOrdEnumCmd declName
+      else
+        mkOrdInstanceCmds declName
+    cmds.forM elabCommand
+
 def mkOrdInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
   if (← declNames.allM isInductive) then
     for declName in declNames do
-      let cmds ← withoutExposeFromCtors declName <| liftTermElabM <| mkOrdInstanceCmds declName
-      cmds.forM elabCommand
+      mkOrdInstance declName
     return true
   else
     return false

src/Lean/Elab/DocString.lean

@@ -12,6 +12,8 @@ public import Lean.Elab.Term.TermElabM
 public import Lean.Elab.Command.Scope
 import Lean.DocString.Syntax
 import Lean.Meta.Hint
+import Lean.DocString.Markdown
+import Lean.BuiltinDocAttr
 
 set_option linter.missingDocs true
 
@@ -22,7 +24,6 @@ open Std
 open scoped Lean.Doc.Syntax
 
 
-
 public section
 
 private structure ElabLink where
@@ -112,8 +113,6 @@ deriving BEq, Repr
 
 /-- Context used as a reader in `DocM`. -/
 structure Context where
-  /-- The declaration for which documentation is being elaborated. -/
-  declName : Name
   /-- Whether suggestions should be provided interactively. -/
   suggestionMode : SuggestionMode
 
@@ -140,32 +139,95 @@ instance : MonadLift TermElabM DocM where
       act
     return v
 
+private structure ModuleDocstringState extends Lean.Doc.State where
+  scopedExts : Array (ScopedEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)
+
+
+private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDocstringState) ←
+  registerEnvExtension (pure none)
+
+private def getModState
+    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
+    [MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
+  if let some st := modDocstringStateExt.getState (← getEnv) then
+    return st
+  else
+    let lctx ← getLCtx
+    let openDecls ← getOpenDecls
+    let options ← getOptions
+    let scopes := [{header := "", isPublic := true}]
+    let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
+    modifyEnv fun env =>
+      modDocstringStateExt.setState env st
+    return st
+
+private def setModState [Monad m] [MonadEnv m] (state : ModuleDocstringState) : m Unit := do
+  modifyEnv fun env =>
+    modDocstringStateExt.setState env state
+
+/--
+Runs a documentation elaborator in the module docstring context.
+-/
+def DocM.execForModule (act : DocM α) (suggestionMode : SuggestionMode := .interactive) :
+    TermElabM α := withoutModifyingEnv do
+  let sc ← scopedEnvExtensionsRef.get
+  let st ← getModState
+  try
+    scopedEnvExtensionsRef.set st.scopedExts
+    let ((v, _), _) ←
+      act.run { suggestionMode } |>.run {} |>.run st.toState
+    pure v
+  finally
+    scopedEnvExtensionsRef.set sc
+
 open Lean.Parser.Term in
 /--
-Runs a documentation elaborator, discarding changes made to the environment.
+Runs a documentation elaborator in a declaration's context, discarding changes made to the
+environment.
 -/
 def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
     (suggestionMode : SuggestionMode := .interactive) :
     TermElabM α := withoutModifyingEnv do
   let some ci := (← getEnv).constants.find? declName
     | throwError "Unknown constant {declName} when building docstring"
-  let (lctx, localInstances) ← buildContext ci.type binders
-  let sc ← scopedEnvExtensionsRef.get
+  let st ← Term.saveState
+  Core.resetMessageLog -- We'll replay the messages after the elab loop
   try
-    let openDecls ← getOpenDecls
-    let options ← getOptions
-    let scopes := [{header := "", isPublic := true}]
-    let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
-      act.run { declName, suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
-    pure v
+    let (lctx, localInstances) ← buildContext ci.type binders
+    let sc ← scopedEnvExtensionsRef.get
+    try
+      let openDecls ← getOpenDecls
+      let options ← getOptions
+      let scopes := [{header := "", isPublic := true}]
+      let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
+        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
+      pure v
+    finally
+      scopedEnvExtensionsRef.set sc
   finally
-    scopedEnvExtensionsRef.set sc
+    let msgs ← Core.getMessageLog
+    st.restore
+    Core.setMessageLog ((← Core.getMessageLog) ++ msgs)
 where
   buildContext (type : Expr) (binders : Syntax) : TermElabM (LocalContext × LocalInstances) := do
-    -- Create a local context with all binders
+    -- Create a local context with all binders. The type will be updated as we introduce parameters.
     let mut type := type
-    let mut localInstances := (← readThe Meta.Context).localInstances
-    let mut lctx := ← getLCtx
+
+    -- We start with a local context that's reset to only include section variables
+    let mut localInstances ← Meta.getLocalInstances
+    let mut lctx ← getLCtx
+    let sectionFVars := (← read).sectionFVars.valuesArray.filterMap fun
+      | .fvar fv => some fv
+      | _ => none
+    repeat
+      if lctx.size = 0 then break
+      if let some decl := lctx.lastDecl then
+        if sectionFVars.any (· == decl.fvarId) then break
+        else
+          lctx := lctx.pop
+          localInstances := localInstances.filter (·.fvar != .fvar decl.fvarId)
+      else break
+
     let names ← binders.getArgs.flatMapM binderNames
     let mut i := 0
     let mut x := none
@@ -724,6 +786,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docRoleExt.add (roleName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -749,8 +813,12 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `inline) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin roleName <|
       mkApp3 (.const ``addBuiltinDocRole []) (toExpr roleName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -766,6 +834,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
     docCodeBlockExt.add (blockName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -788,9 +858,13 @@ builtin_initialize registerBuiltinAttribute {
         pure decl
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin blockName <|
       mkApp3 (.const ``addBuiltinDocCodeBlock [])
         (toExpr blockName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 /-- A suggestion about an applicable code block -/
@@ -872,6 +946,9 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docDirectiveExt.add (directiveName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+
 }
 
 /--
@@ -897,9 +974,13 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `block) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin directiveName <|
       mkApp3 (.const ``addBuiltinDocDirective [])
         (toExpr directiveName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -916,6 +997,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
     docCommandExt.add (commandName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -939,9 +1022,13 @@ builtin_initialize registerBuiltinAttribute {
 
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin commandName <|
       mkApp3 (.const ``addBuiltinDocCommand [])
         (toExpr commandName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 end
 
@@ -959,76 +1046,88 @@ private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → Doc
 @[implemented_by codeBlockSuggestionsUnsafe]
 private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
 
-private unsafe def roleExpandersForUnsafe (roleName : Ident) : TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))) := do
+private def builtinElabName (n : Name) : Option Name :=
+  if (`Lean.Doc).isPrefixOf n then some n
+  else if n matches (.str .anonymous _) then some <| `Lean.Doc ++ n
+  else none
+
+private unsafe def roleExpandersForUnsafe (roleName : Ident) :
+    TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo roleName
+    try some <$> realizeGlobalConstNoOverload roleName
     catch | _ => pure none
   if let some x := x? then
     let names := (docRoleExt.getState (← getEnv)).get? x |>.getD #[]
     let builtins := (← builtinDocRoles.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ builtins.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ builtins
   else
     let x := roleName.getId
     let hasBuiltin :=
       (← builtinDocRoles.get).get? x <|> (← builtinDocRoles.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 
 @[implemented_by roleExpandersForUnsafe]
 private opaque roleExpandersFor (roleName : Ident) :
-  TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))
+  TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))))
 
-private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
+    TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo codeBlockName
+    try some <$> realizeGlobalConstNoOverload codeBlockName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCodeBlockExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCodeBlocks.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := codeBlockName.getId
     let hasBuiltin :=
       (← builtinDocCodeBlocks.get).get? x <|> (← builtinDocCodeBlocks.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 
 @[implemented_by codeBlockExpandersForUnsafe]
-private opaque codeBlockExpandersFor (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque codeBlockExpandersFor (codeBlockName : Ident) :
+  TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def directiveExpandersForUnsafe (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
+    TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo directiveName
+    try some <$> realizeGlobalConstNoOverload directiveName
     catch | _ => pure none
   if let some x := x? then
     let names := (docDirectiveExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocDirectives.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := directiveName.getId
     let hasBuiltin :=
       (← builtinDocDirectives.get).get? x <|> (← builtinDocDirectives.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 @[implemented_by directiveExpandersForUnsafe]
-private opaque directiveExpandersFor (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque directiveExpandersFor (directiveName : Ident) :
+  TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def commandExpandersForUnsafe (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def commandExpandersForUnsafe (commandName : Ident) :
+    TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo commandName
+    try some <$> realizeGlobalConstNoOverload commandName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCommandExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCommands.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := commandName.getId
     let hasBuiltin :=
       (← builtinDocCommands.get).get? x <|> (← builtinDocCommands.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 @[implemented_by commandExpandersForUnsafe]
-private opaque commandExpandersFor (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque commandExpandersFor (commandName : Ident) :
+  TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
 
 private def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
@@ -1117,12 +1216,17 @@ private def mkSuggestion  (ref : Syntax) (hintTitle : MessageData) (newStrings :
       toMessageData <| Diff.linesToString <| d.filter (·.1 != Action.skip)
     pure m!"\n\nHint: {hintTitle}\n{indentD <| m!"\n".joinSep edits.toList}"
 
+def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
+  let env ← getEnv
+  if env.contains x then return x
+  else return `Lean.Doc ++ x
 
 /--
 Elaborates the syntax of an inline document element to an actual inline document element.
 -/
 public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline) :=
-  withRef stx do
+  withRef stx <|
+  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
   match stx with
   | `(inline|$s:str) =>
     return .text s.getString
@@ -1154,14 +1258,15 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {role, args, moreInfo} => do
-            pure {
-              fst :=
-                "{" ++ (← suggestionName role).toString ++
-                (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
-              snd.fst := none
-              snd.snd := moreInfo.map withSpace
-            }
+          let ss : Array (String × Option String × Option String) ←
+            suggestions.mapM fun {role, args, moreInfo} => do
+              pure {
+                fst :=
+                  "{" ++ (← suggestionName role).toString ++
+                  (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
+                snd.fst := none
+                snd.snd := moreInfo.map withSpace
+              }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion stx m!"Insert a role to document it:" ss
           logWarning m!"Code element could be more specific.{hint}"
@@ -1172,9 +1277,15 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
     return .math .display s.getString
   | `(inline|role{$name $args*}[$inl*]) =>
     let expanders ← roleExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex inl args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .role
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1193,7 +1304,8 @@ where
 Elaborates the syntax of an block-level document element to an actual block-level document element.
 -/
 public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline ElabBlock) :=
-  withRef stx do
+  withRef stx <|
+  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
   match stx with
   | `(block|para[$inls*]) =>
     .para <$> inls.mapM elabInline
@@ -1231,9 +1343,15 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     return .empty
   | `(block| ::: $name $args* { $content*}) =>
     let expanders ← directiveExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex content args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .directive
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1253,24 +1371,30 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {name, args, moreInfo} => do
-            pure {
-              fst :=
-                str ++ (← suggestionName name).toString ++
-                (args.map (" " ++ ·)).getD "",
-              snd.fst := moreInfo.map withSpace
-              snd.snd := none
-            }
+          let ss : Array (String × Option String × Option String) ←
+            suggestions.mapM fun {name, args, moreInfo} => do
+              pure {
+                fst :=
+                  str ++ (← suggestionName name).toString ++
+                  (args.map (" " ++ ·)).getD "",
+                snd.fst := moreInfo.map withSpace
+                snd.snd := none
+              }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion opener m!"Insert a specific kind of code block:" ss
           logWarning m!"Code block could be more specific.{hint}"
-
     return .code s.getString
   | `(block| ```$name $args* | $s ```) =>
     let expanders ← codeBlockExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex s args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .codeBlock
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1281,9 +1405,15 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     throwErrorAt name "No code block expander for `{name}`"
   | `(block| command{$name $args*}) =>
     let expanders ← commandExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .command
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1292,6 +1422,12 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
           else throw e
         | e => throw e
     throwErrorAt name "No document command elaborator for `{name}`"
+  | `(block|%%%$_*%%%) =>
+    let h ←
+      if stx.raw.getRange?.isSome then m!"Remove it".hint #[""] (ref? := stx)
+      else pure m!""
+    logError m!"Part metadata is not supported in docstrings.{h}"
+    return .empty
   | other => throwErrorAt other "Unsupported syntax: {other}"
 where
   withSpace (s : String) : String :=
@@ -1314,10 +1450,13 @@ private partial def elabBlocks' (level : Nat) :
         else if n = level then
           set xs
           let (content, subParts) ← elabBlocks' (level + 1)
-          let title ← liftM <| name.mapM elabInline
+          let title ←
+            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := x}) <|
+              name.mapM elabInline
+          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
           sub := sub.push {
             title,
-            titleString := "" -- TODO get string from filemap?
+            titleString := mdTitle
             metadata := none
             content, subParts
           }
@@ -1331,83 +1470,120 @@ private partial def elabBlocks' (level : Nat) :
         catch
           | e =>
             logErrorAt e.getRef e.toMessageData
-    else break
+    else
+      break
   return (pre, sub)
 
+private def elabModSnippet'
+    (range : DeclarationRange) (level : Nat) (blocks : TSyntaxArray `block) :
+    DocM VersoModuleDocs.Snippet := do
+  let mut snippet : VersoModuleDocs.Snippet := {
+    declarationRange := range
+  }
+  let mut maxLevel := level
+  for b in blocks do
+    if let `(block|header($n){$name*}) := b then
+        let n := n.getNat
+        if n > maxLevel then
+          logErrorAt b m!"Incorrect header nesting: expected at most `{"#".pushn '#' maxLevel}` \
+            but got `{"#".pushn '#' n}`"
+        else
+          let title ←
+            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <|
+              name.mapM elabInline
+          let some headerRange ← getDeclarationRange? b
+            | throwErrorAt b "Can't find header source position"
+          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
+          snippet := snippet.addPart n headerRange {
+            title,
+            titleString := mdTitle
+            metadata := none, content := #[], subParts := #[]
+          }
+      else
+        snippet := snippet.addBlock (← elabBlock b)
+  return snippet
+
+private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
+  match inl with
+  | .concat xs => .concat <$> xs.mapM fixupInline
+  | .emph xs => .emph <$> xs.mapM fixupInline
+  | .bold xs => .bold <$> xs.mapM fixupInline
+  | .link content url => (.link · url) <$> content.mapM fixupInline
+  | .footnote name content => .footnote name <$> content.mapM fixupInline
+  | .text s => pure (.text s)
+  | .image alt url => pure (.image alt url)
+  | .code s => pure (.code s)
+  | .math mode s => pure (.math mode s)
+  | .linebreak s => pure (.linebreak s)
+  | .other i@{ name, val } xs =>
+    match name with
+    | ``delayLink =>
+      let some {name} := val.get? ElabLink
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
+        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+        return .link (← xs.mapM fixupInline) url
+      else
+        logErrorAt name "Reference not found"
+        return .concat (← xs.mapM fixupInline)
+    | ``delayImage =>
+      let some {alt, name} := val.get? ElabImage
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
+        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+        return .image alt url
+      else
+        logErrorAt name "Reference not found"
+        return .empty
+    | ``delayFootnote =>
+      let some {name} := val.get? ElabFootnote
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
+        unless seen do modifyThe InternalState fun st =>
+          { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
+        return .footnote nameStr #[← fixupInline content]
+      else
+        logErrorAt name "Footnote not found"
+        return .empty
+    | _ => .other i <$> xs.mapM fixupInline
+
+private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
+  match block with
+  | .para xs => .para <$> xs.mapM fixupInline
+  | .concat xs => .concat <$> xs.mapM fixupBlock
+  | .blockquote xs => .blockquote <$> xs.mapM fixupBlock
+  | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
+    let term ← term.mapM fixupInline
+    let desc ← desc.mapM fixupBlock
+    pure { term, desc }
+  | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
+  | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
+  | .code s => pure (.code s)
+  | .other i xs => .other i <$> xs.mapM fixupBlock
+
+private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
+  return { part with
+    title := ← part.title.mapM fixupInline
+    content := ← part.content.mapM fixupBlock,
+    subParts := ← part.subParts.mapM fixupPart
+  }
+
+
 private partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
   | (bs, ps) => do
-    let bs ← bs.mapM fixB
-    let ps ← ps.mapM fixP
+    let bs ← bs.mapM fixupBlock
+    let ps ← ps.mapM fixupPart
     return (bs, ps)
-where
-  fixI (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
-    match inl with
-    | .concat xs => .concat <$> xs.mapM fixI
-    | .emph xs => .emph <$> xs.mapM fixI
-    | .bold xs => .bold <$> xs.mapM fixI
-    | .link content url => (.link · url) <$> content.mapM fixI
-    | .footnote name content => .footnote name <$> content.mapM fixI
-    | .text s => pure (.text s)
-    | .image alt url => pure (.image alt url)
-    | .code s => pure (.code s)
-    | .math mode s => pure (.math mode s)
-    | .linebreak s => pure (.linebreak s)
-    | .other i@{ name, val } xs =>
-      match name with
-      | ``delayLink =>
-        let some {name} := val.get? ElabLink
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
-          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-          return .link (← xs.mapM fixI) url
-        else
-          logErrorAt name "Reference not found"
-          return .concat (← xs.mapM fixI)
-      | ``delayImage =>
-        let some {alt, name} := val.get? ElabImage
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
-          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-          return .image alt url
-        else
-          logErrorAt name "Reference not found"
-          return .empty
-      | ``delayFootnote =>
-        let some {name} := val.get? ElabFootnote
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
-          unless seen do modifyThe InternalState fun st =>
-            { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
-          return .footnote nameStr #[← fixI content]
-        else
-          logErrorAt name "Footnote not found"
-          return .empty
-      | _ => .other i <$> xs.mapM fixI
-
-  fixB (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
-    match block with
-    | .para xs => .para <$> xs.mapM fixI
-    | .concat xs => .concat <$> xs.mapM fixB
-    | .blockquote xs => .blockquote <$> xs.mapM fixB
-    | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
-      let term ← term.mapM fixI
-      let desc ← desc.mapM fixB
-      pure { term, desc }
-    | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
-    | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
-    | .code s => pure (.code s)
-    | .other i xs => .other i <$> xs.mapM fixB
-
-  fixP (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
-    return { part with
-      title := ← part.title.mapM fixI
-      content := ← part.content.mapM fixB,
-      subParts := ← part.subParts.mapM fixP
-    }
 
+private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
+  return {snippet with
+    text := ← snippet.text.mapM fixupBlock,
+    sections := ← snippet.sections.mapM fun (level, range, content) => do
+      return (level, range, ← fixupPart content)
+  }
 /--
 After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
@@ -1419,10 +1595,19 @@ private def warnUnusedRefs : DocM Unit := do
     unless seen do
       logWarningAt location "Unused footnote"
 
-/-- Elaborates a sequence of blocks into a document -/
+/-- Elaborates a sequence of blocks into a document. -/
 public def elabBlocks (blocks : TSyntaxArray `block) :
     DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
   let (v, _) ← elabBlocks' 0 |>.run blocks
   let res ← fixupBlocks v
   warnUnusedRefs
   return res
+
+/-- Elaborates a sequence of blocks into a module doc snippet. -/
+public def elabModSnippet
+    (range : DeclarationRange) (blocks : TSyntaxArray `block) (nestingLevel : Nat) :
+    DocM (VersoModuleDocs.Snippet) := do
+  let s ← elabModSnippet' range nestingLevel blocks
+  let s ← fixupSnippet s
+  warnUnusedRefs
+  return s

src/Lean/Elab/InfoTree/Main.lean

@@ -221,6 +221,12 @@ def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
   f!"[Choice] @ {formatElabInfo ctx info.toElabInfo}"
 
+def DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format :=
+  f!"[Doc] {info.stx.getKind} @ {formatElabInfo ctx info.toElabInfo}"
+
+def DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format :=
+  f!"[DocElab] {info.name} ({repr info.kind}) @ {formatElabInfo ctx info.toElabInfo}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
@@ -237,6 +243,8 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
   | ofDelabTermInfo i      => i.format ctx
   | ofChoiceInfo i         => pure <| i.format ctx
+  | ofDocInfo i            => pure <| i.format ctx
+  | ofDocElabInfo i        => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
@@ -254,6 +262,8 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofFieldRedeclInfo _    => none
   | ofDelabTermInfo i      => some i.toElabInfo
   | ofChoiceInfo i         => some i.toElabInfo
+  | ofDocInfo i            => some i.toElabInfo
+  | ofDocElabInfo i        => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.

src/Lean/Elab/InfoTree/Types.lean

@@ -207,6 +207,23 @@ the language server provide interactivity even when all overloaded elaborators f
 -/
 structure ChoiceInfo extends ElabInfo where
 
+inductive DocElabKind where
+  | role | codeBlock | directive | command
+deriving Repr
+
+/--
+Indicates that an extensible document elaborator was used here.
+-/
+structure DocElabInfo extends ElabInfo where
+  name : Name
+  kind : DocElabKind
+
+/--
+Indicates that a piece of syntax was elaborated as documentation.
+-/
+structure DocInfo extends ElabInfo where
+
+
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
@@ -224,6 +241,8 @@ inductive Info where
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
   | ofDelabTermInfo (i : DelabTermInfo)
   | ofChoiceInfo (i : ChoiceInfo)
+  | ofDocInfo (i : DocInfo)
+  | ofDocElabInfo (i : DocElabInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -6,24 +6,23 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Eqns
-public import Lean.Meta.CtorRecognizer
-public import Lean.Util.CollectFVars
-public import Lean.Util.ForEachExprWhere
-public import Lean.Meta.Tactic.Split
-public import Lean.Meta.Tactic.Apply
-public import Lean.Meta.Tactic.Refl
-public import Lean.Meta.Match.MatchEqs
-public import Lean.DefEqAttrib
+public import Lean.Meta.Basic
+import Lean.Meta.Eqns
+import Lean.Meta.CtorRecognizer
+import Lean.Util.CollectFVars
+import Lean.Util.ForEachExprWhere
+import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Refl
+import Lean.Meta.Match.MatchEqs
+import Lean.DefEqAttrib
 import Lean.Meta.Tactic.SplitIf
 import Lean.Meta.Tactic.Simp.Main
 
-public section
-
 namespace Lean.Elab.Eqns
 open Meta
 
-structure EqnInfoCore where
+public structure EqnInfoCore where
   declName    : Name
   levelParams : List Name
   type        : Expr
@@ -46,7 +45,7 @@ def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let (true, rhs') := expand false rhs | return none
   return some (← mvarId.replaceTargetDefEq (← mkEq lhs rhs'))
 
-def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
+public def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
   let mvarId' ← Split.simpMatchTarget mvarId
   if mvarId != mvarId' then return some mvarId' else return none
 
@@ -54,7 +53,7 @@ def simpMatch? (mvarId : MVarId) : MetaM (Option MVarId) := do
 Simplify `if-then-expression`s in the goal target.
 If `useNewSemantics` is `true`, the flag `backward.split` is ignored.
 -/
-def simpIf? (mvarId : MVarId) (useNewSemantics := false) : MetaM (Option MVarId) := do
+public def simpIf? (mvarId : MVarId) (useNewSemantics := false) : MetaM (Option MVarId) := do
   let mvarId' ← simpIfTarget mvarId (useDecide := true) (useNewSemantics := useNewSemantics)
   if mvarId != mvarId' then return some mvarId' else return none
 
@@ -117,7 +116,7 @@ private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
       dependsOn type fvarId
 
 /-- Try to close goal using `rfl` with smart unfolding turned off. -/
-def tryURefl (mvarId : MVarId) : MetaM Bool :=
+public def tryURefl (mvarId : MVarId) : MetaM Bool :=
   withOptions (smartUnfolding.set · false) do
     try mvarId.refl; return true catch _ => return false
 
@@ -232,7 +231,7 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+public partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run #[]
   return eqnTypes
 where
@@ -258,7 +257,7 @@ where
   Alternative solution: improve `saveEqn` and make sure it never includes unnecessary hypotheses.
   These hypotheses are leftovers from tactics such as `splitMatch?` used in `mkEqnTypes`.
 -/
-def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr) := do
+public def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr) := do
   go declType declValue #[] {}
 where
   go (type value : Expr) (xs : Array Expr) (lctx : LocalContext) : CoreM (Expr × Expr) := do
@@ -283,7 +282,7 @@ where
         return (lctx.mkForall xsNew type, lctx.mkLambda xsNew value)
 
 /-- Delta reduce the equation left-hand-side -/
-def deltaLHS (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+public def deltaLHS (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | throwTacticEx `deltaLHS mvarId "equality expected"
   let some lhs ← delta? lhs | throwTacticEx `deltaLHS mvarId "failed to delta reduce lhs"
@@ -303,7 +302,7 @@ private partial def whnfAux (e : Expr) : MetaM Expr := do
   | _ => return e
 
 /-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/
-def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
+public def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
   let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | return none
   let lhs' ← whnfAux lhs
@@ -312,7 +311,7 @@ def whnfReducibleLHS? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withCo
   else
     return none
 
-def tryContradiction (mvarId : MVarId) : MetaM Bool := do
+public def tryContradiction (mvarId : MVarId) : MetaM Bool := do
   mvarId.contradictionCore { genDiseq := true }
 
 /--
@@ -407,7 +406,7 @@ proves them using `mkEqnProof`.
 This is currently used for non-recursive functions, well-founded recursion and partial_fixpoint,
 but not for structural recursion.
 -/
-def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
+public def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do
   trace[Elab.definition.eqns] "mkEqns: {.ofConstName declName}"
   let info ← getConstInfoDefn declName
   let us := info.levelParams.map mkLevelParam
@@ -448,7 +447,7 @@ where
   We basically keep splitting the `match` and `if-then-else` expressions in the right hand side
   until one of the equational theorems is applicable.
 -/
-partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
+public partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
   let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for `{.ofConstName declName}`"
   let tryEqns (mvarId : MVarId) : MetaM Bool :=
     eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do

src/Lean/Elab/PreDefinition/Nonrec/Eqns.lean

@@ -6,14 +6,12 @@ Authors: Leonardo de Moura, Joachim Breitner
 module
 
 prelude
-public import Lean.Meta.Tactic.Rewrite
-public import Lean.Meta.Tactic.Split
-public import Lean.Elab.PreDefinition.Basic
-public import Lean.Elab.PreDefinition.Eqns
-public import Lean.Meta.ArgsPacker.Basic
-public import Init.Data.Array.Basic
-
-public section
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Eqns
+import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
 
 namespace Lean.Elab.Nonrec
 open Meta
@@ -22,7 +20,7 @@ open Eqns
 /--
 Simple, coarse-grained equation theorem for nonrecursive definitions.
 -/
-private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
+def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
   if let some (.defnInfo info) := (← getEnv).find? declName then
     let name := mkEqLikeNameFor (← getEnv) declName eqn1ThmSuffix
     trace[Elab.definition.eqns] "mkSimpleEqnThm: {name}"

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -6,35 +6,32 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Elab.PreDefinition.Basic
 public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.FixedParams
-public import Lean.Meta.ArgsPacker.Basic
-public import Init.Data.Array.Basic
-public import Init.Internal.Order.Basic
+import Lean.Meta.ArgsPacker.Basic
+import Init.Data.Array.Basic
+import Init.Internal.Order.Basic
 import Lean.Elab.Tactic.Conv
 import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Split
 
-public section
-
 namespace Lean.Elab.PartialFixpoint
 open Meta
 open Eqns
 
-structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
   fixedParamPerms : FixedParamPerms
   fixpointType    : Array PartialFixpointType
   deriving Inhabited
 
-builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
+public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
     -- Do not export for non-exposed defs
     s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
+public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name)
     (fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType): MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   unless preDefs.all fun p => p.kind.isTheorem do
@@ -66,7 +63,7 @@ partial def rwFixUnder (lhs : Expr) : MetaM Expr := do
   else
     throwError "rwFixUnder: unexpected expression {lhs}"
 
-private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
+def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let mut mvarId := mvarId
   let target ← mvarId.getType'
   let some (_, lhs, rhs) := target.eq? | unreachable!

src/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean

@@ -7,19 +7,18 @@ Authors: Joachim Breitner
 module
 
 prelude
-public import Lean.Meta.Basic
-public import Lean.Meta.Match.MatcherApp.Transform
-public import Lean.Meta.Check
-public import Lean.Meta.Tactic.Subst
-public import Lean.Meta.Injective -- for elimOptParam
-public import Lean.Meta.ArgsPacker
-public import Lean.Meta.PProdN
-public import Lean.Meta.Tactic.Apply
-public import Lean.Elab.PreDefinition.PartialFixpoint.Eqns
-public import Lean.Elab.Command
-public import Lean.Meta.Tactic.ElimInfo
-
-public section
+import Lean.Meta.Basic
+import Lean.Meta.Match.MatcherApp.Transform
+import Lean.Meta.Check
+import Lean.Meta.Tactic.Subst
+import Lean.Meta.Injective -- for elimOptParam
+import Lean.Meta.ArgsPacker
+import Lean.Meta.PProdN
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.PreDefinition.PartialFixpoint.Eqns
+import Lean.Elab.Command
+import Lean.Meta.Tactic.ElimInfo
+import Init.Internal.Order.Basic
 
 namespace Lean.Elab.PartialFixpoint
 
@@ -42,7 +41,7 @@ partial def mkAdmProj (packedInst : Expr) (i : Nat) (e : Expr) : MetaM Expr := d
     assert! i == 0
     return e
 
-@[expose] def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do
+def CCPOProdProjs (n : Nat) (inst : Expr) : Array Expr := Id.run do
   let mut insts := #[inst]
   while insts.size < n do
     let inst := insts.back!
@@ -368,7 +367,7 @@ def mkOptionAdm (motive : Expr) : MetaM Expr := do
     inst ← mkAppOptM ``admissible_pi #[none, none, none, none, inst]
     for y in ys.reverse do
       inst ← mkLambdaFVars #[y] inst
-      inst ← mkAppOptM ``admissible_pi_apply #[none, none, none, none, inst]
+      inst ← mkAppOptM ``Order.admissible_pi_apply #[none, none, none, none, inst]
     pure inst
 
 def derivePartialCorrectness (name : Name) (isConclusionMutual : Bool) : MetaM Unit := do

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -6,16 +6,16 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Eqns
-public import Lean.Meta.Tactic.Split
-public import Lean.Meta.Tactic.Simp.Main
-public import Lean.Meta.Tactic.Apply
-public import Lean.Elab.PreDefinition.Basic
+public import Lean.Meta.Basic
 public import Lean.Elab.PreDefinition.Eqns
 public import Lean.Elab.PreDefinition.FixedParams
-public import Lean.Elab.PreDefinition.Structural.Basic
-
-public section
+import Lean.Meta.Eqns
+import Lean.Meta.Tactic.Split
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Meta.Tactic.Apply
+import Lean.Elab.PreDefinition.Basic
+import Lean.Elab.PreDefinition.Structural.Basic
+import Lean.Meta.Match.MatchEqs
 
 namespace Lean.Elab
 open Meta
@@ -23,7 +23,7 @@ open Eqns
 
 namespace Structural
 
-structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo extends EqnInfoCore where
   recArgPos : Nat
   declNames : Array Name
   fixedParamPerms : FixedParamPerms
@@ -138,12 +138,12 @@ where
     }
     inferDefEqAttr name
 
-builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
+public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
     -- Do not export for non-exposed defs
     s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
 
-def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
+public def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
     (fixedParamPerms : FixedParamPerms) : CoreM Unit := do
   ensureEqnReservedNamesAvailable preDef.declName
   modifyEnv fun env => eqnInfoExt.insert env preDef.declName

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -6,33 +6,31 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Tactic.Rewrite
-public import Lean.Meta.Tactic.Split
-public import Lean.Elab.PreDefinition.Basic
 public import Lean.Elab.PreDefinition.Eqns
-public import Lean.Meta.ArgsPacker.Basic
 public import Lean.Elab.PreDefinition.FixedParams
-public import Init.Data.Array.Basic
-
-public section
+public import Lean.Meta.ArgsPacker.Basic
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Split
+import Lean.Elab.PreDefinition.Basic
+import Init.Data.Array.Basic
 
 namespace Lean.Elab.WF
 open Meta
 open Eqns
 
-structure EqnInfo extends EqnInfoCore where
+public structure EqnInfo extends EqnInfoCore where
   declNames       : Array Name
   declNameNonRec  : Name
   argsPacker      : ArgsPacker
   fixedParamPerms : FixedParamPerms
   deriving Inhabited
 
-builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
+public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
   mkMapDeclarationExtension (exportEntriesFn := fun env s _ =>
     -- Do not export for non-exposed defs
     s.filter (fun n _ => env.find? n |>.any (·.hasValue)) |>.toArray)
 
-def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
+public def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms)
     (argsPacker : ArgsPacker) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-

src/Lean/Elab/PreDefinition/WF/Unfold.lean

@@ -13,6 +13,8 @@ import Lean.Meta.Tactic.Split
 public import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs
+import Lean.Meta.Tactic.Delta
+import Lean.Meta.Tactic.Refl
 
 /-!
 This module is responsible for proving the unfolding equation for functions defined

src/Lean/Elab/Tactic/Do/VCGen.lean

@@ -6,7 +6,6 @@ Authors: Sebastian Graf
 module
 
 prelude
-import Std.Do.WP
 import Std.Do.Triple
 import Lean.Elab.Tactic.Do.VCGen.Split
 import Lean.Elab.Tactic.Simp
@@ -21,8 +20,10 @@ import Lean.Elab.Tactic.Do.Spec
 import Lean.Elab.Tactic.Do.Attr
 import Lean.Elab.Tactic.Do.Syntax
 import Lean.Elab.Tactic.Induction
+import Lean.Meta.Tactic.TryThis
 
 public import Lean.Elab.Tactic.Do.VCGen.Basic
+import Lean.Elab.Tactic.Do.VCGen.SuggestInvariant
 
 public section
 
@@ -362,14 +363,14 @@ where
 
 end VCGen
 
-def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TacticM Unit := do
+def elabInvariants (stx : Syntax) (invariants : Array MVarId) (suggestInvariant : MVarId → TacticM Term) : TacticM Unit := do
   let some stx := stx.getOptional? | return ()
   let stx : TSyntax ``invariantAlts := ⟨stx⟩
   withRef stx do
   match stx with
-  | `(invariantAlts| invariants $alts*) =>
+  | `(invariantAlts| $invariantsKW $alts*) =>
     let invariants ← invariants.filterM (not <$> ·.isAssigned)
-    for h : n in [0:alts.size] do
+    for h : n in 0...alts.size do
       let alt := alts[n]
       match alt with
       | `(invariantAlt| · $rhs) =>
@@ -378,9 +379,25 @@ def elabInvariants (stx : Syntax) (invariants : Array MVarId) : TacticM Unit :=
           continue
         discard <| evalTacticAt (← `(tactic| exact $rhs)) mv
       | _ => logErrorAt alt m!"Expected invariantAlt, got {alt}"
-    if alts.size < invariants.size then
-      let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
-      throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
+    if let `(invariantsKW| invariants) := invariantsKW then
+      if alts.size < invariants.size then
+        let missingTypes ← invariants[alts.size:].toArray.mapM (·.getType)
+        throwErrorAt stx m!"Lacking definitions for the following invariants.\n{toMessageList missingTypes}"
+    else
+      -- Otherwise, we have `invariants?`. Suggest missing invariants.
+      let mut suggestions := #[]
+      for i in 0...invariants.size do
+        let mv := invariants[i]!
+        if ← mv.isAssigned then
+          continue
+        let invariant ← suggestInvariant mv
+        suggestions := suggestions.push (← `(invariantAlt| · $invariant))
+      let alts' := alts ++ suggestions
+      let stx' ← `(invariantAlts|invariants $alts'*)
+      if suggestions.size > 0 then
+        Lean.Meta.Tactic.TryThis.addSuggestion stx stx'
+      else
+        logInfoAt stx m!"There were no suggestions for missing invariants."
   | _ => logErrorAt stx m!"Expected invariantAlts, got {stx}"
 
 private def patchVCAltIntoCaseTactic (alt : TSyntax ``vcAlt) : TSyntax ``case :=
@@ -432,7 +449,7 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
       Tactic.run vc (Tactic.evalTactic tac *> Tactic.pruneSolvedGoals)
   let invariants ← Term.TermElabM.run' do
     let invariants ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) invariants else pure invariants
-  elabInvariants stx[3] invariants
+  elabInvariants stx[3] invariants (suggestInvariant vcs)
   let vcs ← Term.TermElabM.run' do
     let vcs ← if ctx.config.trivial then runOnVCs (← `(tactic| try mvcgen_trivial)) vcs else pure vcs
     let vcs ← if ctx.config.leave then runOnVCs (← `(tactic| try mleave)) vcs else pure vcs

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -181,6 +181,10 @@ partial def reduceProjBeta? (e : Expr) : MetaM (Option Expr) :=
           let e' := mkAppRev f' rargs
           go (some e') e'.getAppFn e'.getAppRevArgs
         | none    => pure lastReduction
+      | .letE x ty val body nondep =>
+        match ← go none body rargs with
+        | none => pure lastReduction
+        | some body' => pure (some (.letE x ty val body' nondep))
       | _ => pure lastReduction
 
 def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do

src/Lean/Elab/Tactic/Do/VCGen/SuggestInvariant.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+module
+
+prelude
+public import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Simp.Rewrite
+import Lean.Util.OccursCheck
+import Std.Do.Triple
+import Std.Tactic.Do -- Needed for use of `mleave` in quote
+
+public section
+
+namespace Lean.Elab.Tactic.Do
+
+open Lean Elab Tactic Meta
+open Std.Do
+
+private def duplicateMVar (m : MVarId) : MetaM MVarId := do
+  let d ← m.getDecl
+  let e ← mkFreshExprMVarAt d.lctx d.localInstances d.type d.kind d.userName d.numScopeArgs
+  return e.mvarId!
+
+private def eraseMacroScopesFromSyntax : Syntax → Syntax
+  | Syntax.ident info rawVal val preresolved =>
+    Syntax.ident info rawVal val.eraseMacroScopes preresolved
+  | Syntax.node info kind args =>
+    Syntax.node info kind (args.map eraseMacroScopesFromSyntax)
+  | Syntax.atom info val => Syntax.atom info val
+  | Syntax.missing => Syntax.missing
+
+private def eraseMacroScopesFromTSyntax (syn : TSyntax name) : TSyntax name :=
+  ⟨eraseMacroScopesFromSyntax syn.raw⟩
+
+/--
+Returns `some (ρ, σ)` if `doStateTupleTy` is of the form `MProd (Option ρ) σ` and every VC in `vcs`
+uses the `Option ρ` component according to early return semantics.
+* `ρ` is the type of early return (`Unit` in case of `break`)
+* `σ` is an `n`-ary `MProd`, carrying the current value of the `let mut` variables.
+  NB: When `n=0`, we have `MProd (Option ρ) PUnit` rather than `Option ρ`.
+-/
+private def hasEarlyReturn (vcs : Array MVarId) (inv : MVarId) (doStateTupleTy : Expr) : MetaM (Option (Expr × Expr)) := do
+  if !(doStateTupleTy.isAppOf ``MProd) || doStateTupleTy.getAppNumArgs < 2 then return none
+  let_expr Option ρ := doStateTupleTy.getArg! 0 | return none
+  let σ := doStateTupleTy.getArg! 1
+
+  -- The predicate on `doStateTupleTy` above is not sufficient; after all the user might just have
+  -- introduced `let mut ret : Option α` and not use this variable according to "early return
+  -- semantics", meaning that *if* `ret = some r` for some `r : ρ`, then the loop body returns
+  -- `ForInStep.done (ret, ...)`. This is a property upheld by the `do` elaborator.
+  --
+  -- At this point, `mvcgen` has already run, so we do not see the syntax of the original loop body.
+  -- However, we know that loop invariant lemmas such as `Spec.forIn_list` require that the
+  -- invariant holds at `suffix = []` whenever the loop body returns `ForInStep.done`.
+  -- Therefore, a sufficient condition for early return depends on whether all the VCs conform to
+  -- the property:
+  --
+  -- > For any use of `?inv` of the form `?inv.fst (cursor, ⟨ret, ...⟩)` it is provable that either
+  -- > `ret = none` or `cursor.suffix = []`.
+  --
+  -- Examples of VC goal types that uphold the property:
+  -- * `(Prod.fst ?inv ({ «prefix» := [], suffix := l, property := ⋯ }, ⟨none, PUnit.unit⟩)).down`
+  --   because `ret=none`
+  -- * `(Prod.fst ?inv ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, ⟨none, PUnit.unit⟩)).down`
+  --   because `ret=none`
+  -- * `(Prod.fst ?inv ({ «prefix» := l, suffix := [], property := ⋯ }, ⟨some true, PUnit.unit⟩)).down`
+  --   because `suffix = []`
+  -- Example of a VC not fulfilling the property:
+  -- * `(Prod.fst ?inv ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, ⟨some cur✝, ()⟩)).down`
+  --   because `ret = some _` and `suffix = suff✝` and `suff✝` has instances other than `[]`.
+  -- And similarly for unsimplified entailment `_ ⊢ₛ Prod.fst ?inv (cursor, ⟨some r, ...⟩)`:
+  -- * `_ ⊢ₛ Prod.fst ?inv ({ «prefix» := pref✝ ++ [cur✝], suffix := suff✝, property := ⋯ }, ⟨some cur✝, ()⟩)`
+  --   because `ret = some _` and `suffix = suff✝` and `suff✝` has instances other than `[]`.
+  --
+  -- Hence we check all VCs for the property above.
+
+  for vc in vcs do
+    -- No point in traversing the VC if the invariant is not used in it.
+    let type ← instantiateMVars (← vc.getType)
+    if ← occursCheck inv type then continue
+    -- log m!"Looking at {vc}."
+    let some spredTarget :=
+      if type.isAppOf ``ULift.down && type.getAppNumArgs > 1 then some (type.getArg! 1)
+      else if type.isAppOf ``Std.Tactic.Do.MGoalEntails && type.getAppNumArgs > 2 then some (type.getArg! 2)
+      else if type.isAppOf ``SPred.entails && type.getAppNumArgs > 2 then some (type.getArg! 2)
+      else none
+      | continue
+    -- `spredTarget` should be an overapplication of `Prod.fst`: `spredTarget = Prod.fst ?inv payload args`
+    -- `args` can be non-empty when `σs` is non-empty.
+    if !spredTarget.isAppOf ``Prod.fst then continue
+    let args := spredTarget.getAppArgs
+    -- log m!"Found Prod.fst. Args: {args}"
+    if args.size < 4 then continue -- not an overapplication. Types should prohibit this case
+    if args[2]! != mkMVar inv then continue -- not ?inv that is applied
+    let payload := args[3]!
+    -- log m!"Payload: {payload}"
+
+    let_expr Prod.mk _ _ cursor acc := payload | return none -- NB: be conservative here
+    let_expr List.Cursor.mk _α _l _pref suff _prop := cursor | return none -- dito
+    -- The following check could be smarter. Essentially it tries to construct a proof that
+    -- `suff = []` or `acc = (none, _)` and returns `none` upon failure.
+    if !suff.isAppOf ``List.nil && !(acc.isAppOf ``MProd.mk && (acc.getArg! 2 |>.isAppOf ``Option.none)) then
+      -- log m!"No early return! Not a `List.nil`: {suff} and not an `Option.none`: {acc.getArg! 2}"
+      return none
+  return (ρ, σ)
+
+/--
+Based on how a given metavariable `inv` binding a `Std.Do.Invariant` is used in the `vcs`, suggest
+an initial assignment for `inv` to fill in for the user.
+-/
+def suggestInvariant (vcs : Array MVarId) (inv : MVarId) : TacticM Term := do
+  -- We only synthesize suggestions for invariant subgoals
+  let invType ← instantiateMVars (← inv.getType)
+  let_expr _c@Std.Do.Invariant _α _l doStateTupleTy _ps := invType
+    | throwError "Expected invariant type, got {invType}"
+
+  -- Simplify the VCs a bit using `mleave`. Makes the job of the analysis below simpler.
+  let vcs ← vcs.flatMapM fun vc =>
+    try
+      (·.toArray) <$> evalTacticAt (← `(tactic| mleave)) (← duplicateMVar vc)
+    catch _e =>
+      -- log m!"Failed to simplify {vc}: {_e.toMessageData}"
+      pure #[vc]
+
+  inv.withContext do
+  -- When the loop has an early return, we want to suggest an invariant using `Invariant.withEarlyReturn`.
+  if let some (_ρ, _σ) ← hasEarlyReturn vcs inv doStateTupleTy then
+    -- log m!"Found early return for {inv}!"
+    -- I tried to construct the Expr directly below, but elaborating and then delaborating `_` felt
+    -- strange; furthermore calling the delaborator felt wrong. I might resurrect this code once
+    -- the suggested invariants become deeper, though.
+    --let us := c.constLevels!
+    --withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _
+    --let onContinue ← withLocalDeclsDND #[(`xs, mkApp2 (mkConst ``List.Cursor us) α l), (`acc, σ)] fun _ => _dunno
+    --let onReturn ← withLocalDeclsDND #[(`r, ρ), (`acc, σ)] fun _ => _dunno
+    --let onExcept := mkConst ``ExceptConds.false us
+    --let e := mkApp8 (mkConst ``Std.Do.Invariant.withEarlyReturn us) ps α l σ ρ onContinue onReturn onExcept
+    -- how to delab `e : Expr` back into a `Term` to show to the user?
+    let t ← ``(Invariant.withEarlyReturn (onReturn := fun r acc => _) (onContinue := fun xs acc => _))
+    -- log m!"Suggested invariant: {toString t}"
+    -- log m!"Suggested invariant: {toMessageData t}"
+    return eraseMacroScopesFromTSyntax t
+  eraseMacroScopesFromTSyntax <$> `(⇓ ⟨xs, acc⟩ => _)

src/Lean/Elab/Tactic/Grind.lean

@@ -70,13 +70,14 @@ def elabInitGrindNorm : CommandElab := fun stx =>
   | _ => throwUnsupportedSyntax
 
 private def warnRedundantEMatchArg (s : Grind.EMatchTheorems) (declName : Name) : MetaM Unit := do
+  let minIndexable := false -- TODO: infer it
   let kinds ← match s.getKindsFor (.decl declName) with
     | [] => return ()
-    | [k] => pure m!"@{k.toAttribute}"
+    | [k] => pure m!"@{k.toAttribute minIndexable}"
     | [.eqLhs gen, .eqRhs _]
-    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute}"
+    | [.eqRhs gen, .eqLhs _] => pure m!"@{(Grind.EMatchTheoremKind.eqBoth gen).toAttribute minIndexable}"
     | ks =>
-      let ks := ks.map fun k => m!"@{k.toAttribute}"
+      let ks := ks.map fun k => m!"@{k.toAttribute minIndexable}"
       pure m!"{ks}"
   logWarning m!"this parameter is redundant, environment already contains `{declName}` annotated with `{kinds}`"
 
@@ -132,7 +133,7 @@ where
       for thm in thms do
         params := { params with extra := params.extra.push thm }
     | .ematch kind =>
-      params ← withRef p <| addEMatchTheorem params declName kind minIndexable
+      params ← withRef p <| addEMatchTheorem params id declName kind minIndexable
     | .cases eager =>
       ensureNoMinIndexable minIndexable
       withRef p <| Grind.validateCasesAttr declName eager
@@ -140,7 +141,7 @@ where
     | .intro =>
       if let some info ← Grind.isCasesAttrPredicateCandidate? declName false then
         for ctor in info.ctors do
-          params ← withRef p <| addEMatchTheorem params ctor (.default false) minIndexable
+          params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
       else
         throwError "invalid use of `intro` modifier, `{.ofConstName declName}` is not an inductive predicate"
     | .inj =>
@@ -155,17 +156,17 @@ where
           -- If it is an inductive predicate,
           -- we also add the constructors (intro rules) as E-matching rules
           for ctor in info.ctors do
-            params ← withRef p <| addEMatchTheorem params ctor (.default false) minIndexable
+            params ← withRef p <| addEMatchTheorem params id ctor (.default false) minIndexable
       else
-        params ← withRef p <| addEMatchTheorem params declName (.default false) minIndexable
+        params ← withRef p <| addEMatchTheorem params id declName (.default false) minIndexable (suggest := true)
     | .symbol prio =>
       ensureNoMinIndexable minIndexable
       params := { params with symPrios := params.symPrios.insert declName prio }
     return params
 
-  addEMatchTheorem (params : Grind.Params) (declName : Name)
+  addEMatchTheorem (params : Grind.Params) (id : Ident) (declName : Name)
       (kind : Grind.EMatchTheoremKind)
-      (minIndexable : Bool) : MetaM Grind.Params := do
+      (minIndexable : Bool) (suggest : Bool := false) : MetaM Grind.Params := do
     let info ← getAsyncConstInfo declName
     match info.kind with
     | .thm | .axiom | .ctor =>
@@ -181,7 +182,10 @@ where
       | _ =>
         if kind matches .eqLhs _ | .eqRhs _ then
           ensureNoMinIndexable minIndexable
-        let thm ← Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
+        let thm ← if suggest && !Grind.backward.grind.inferPattern.get (← getOptions) then
+          Grind.mkEMatchTheoremAndSuggest id declName params.symPrios minIndexable (isParam := true)
+        else
+          Grind.mkEMatchTheoremForDecl declName kind params.symPrios (minIndexable := minIndexable)
         if params.ematch.containsWithSamePatterns thm.origin thm.patterns then
           warnRedundantEMatchArg params.ematch declName
         return { params with extra := params.extra.push thm }

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -243,9 +243,10 @@ def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
               -- computation that `noConfusionType h` is equal to `$kType → P`
               let kType ← mkNoConfusionCtorArg ctor P
               let kType := kType.beta (xs ++ fields1 ++ fields2)
-              withLocalDeclD `k kType fun k =>
+              withLocalDeclD `k kType fun k => do
                 let e := mkConst noConfusionName (v :: us)
                 let e := mkAppN e (xs ++ indices ++ #[P, ctor1, ctor2, h, k])
+                let e ← mkExpectedTypeHint e P
                 mkLambdaFVars (xs ++ #[P] ++ ys ++ #[h, k]) e
       let name := ctor.str "noConfusion"
       addDecl (.defnDecl (← mkDefinitionValInferringUnsafe

src/Lean/Meta/LazyDiscrTree.lean

@@ -427,7 +427,7 @@ def targetPath (e : Expr) : MetaM (Array Key) := do
   buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /- Monad for finding matches while resolving deferred patterns. -/
-@[reducible]
+@[reducible, expose /- for codegen -/]
 def MatchM α := StateRefT (Array (Trie α)) MetaM
 
 def runMatch (d : LazyDiscrTree α) (m : MatchM α β)  : MetaM (β × LazyDiscrTree α) := do

src/Lean/Meta/Tactic/FunInd.lean

@@ -23,6 +23,7 @@ import Lean.Elab.Command
 import Lean.Meta.Tactic.ElimInfo
 import Lean.Meta.Tactic.FunIndInfo
 import Lean.Data.Array
+import Lean.Meta.Tactic.Simp.Rewrite
 
 /-!
 This module contains code to derive, from the definition of a recursive function (structural or

src/Lean/Meta/Tactic/Grind.lean

@@ -39,6 +39,7 @@ public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.AC
 public import Lean.Meta.Tactic.Grind.VarRename
 public import Lean.Meta.Tactic.Grind.ProofUtil
+public import Lean.Meta.Tactic.Grind.PropagateInj
 
 public section
 
@@ -80,7 +81,7 @@ builtin_initialize registerTraceClass `grind.debug.final
 builtin_initialize registerTraceClass `grind.debug.forallPropagator
 builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
-builtin_initialize registerTraceClass `grind.debug.ematch.activate
+builtin_initialize registerTraceClass `grind.debug.theorem.activate
 builtin_initialize registerTraceClass `grind.debug.ematch.pattern
 builtin_initialize registerTraceClass `grind.debug.beta
 builtin_initialize registerTraceClass `grind.debug.internalize

src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.ExprPtr
-
 public section
-
 namespace Lean.Meta.Grind
 
 private def hashChild (e : Expr) : UInt64 :=

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Init.Data.Int.OfNat
+import Init.Grind.Propagator
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Init.Data.Int.OfNat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Simp.Arith.Int
 import Lean.Meta.Tactic.Grind.PropagatorAttr

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean

@@ -49,7 +49,12 @@ private def hasTheoryVar (e : Expr) : GoalM Bool := do
 private def isInterpreted (e : Expr) : GoalM Bool := do
   if isInterpretedTerm e then return true
   let f := e.getAppFn
-  return f.isConstOf ``LE.le || f.isConstOf ``Dvd.dvd
+  /-
+  **Note**: `grind` normalizes terms, but some of them cannot be rewritten by `simp` because
+  the rewrite would produce a type incorrect term. Thus, we may have `LT.lt` applications in
+  the goal.
+  -/
+  return f.isConstOf ``LE.le || f.isConstOf ``Dvd.dvd || f.isConstOf ``LT.lt
 
 private def eqAssignment (a b : Expr) : GoalM Bool := do
   let some v₁ ← getAssignmentExt? a | return false

src/Lean/Meta/Tactic/Grind/Arith/Main.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Propagator
 import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Arith.Offset.Types
 import Lean.Meta.Tactic.Grind.Arith.Offset.Main

src/Lean/Meta/Tactic/Grind/Attr.lean

@@ -25,9 +25,11 @@ inductive AttrKind where
 def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do
   match stx with
   | `(Parser.Attr.grindMod|=) => return .ematch (.eqLhs false)
+  | `(Parser.Attr.grindMod|.) => return .ematch (.default false)
   | `(Parser.Attr.grindMod|= gen) => return .ematch (.eqLhs true)
   | `(Parser.Attr.grindMod|→) => return .ematch .fwd
   | `(Parser.Attr.grindMod|←) => return .ematch (.bwd false)
+  | `(Parser.Attr.grindMod|. gen) => return .ematch (.default true)
   | `(Parser.Attr.grindMod|← gen) => return .ematch (.bwd true)
   | `(Parser.Attr.grindMod|=_) => return .ematch (.eqRhs false)
   | `(Parser.Attr.grindMod|=_ gen) => return .ematch (.eqRhs true)

src/Lean/Meta/Tactic/Grind/Beta.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Returns all lambda expressions in the equivalence class with root `root`. -/

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -74,40 +74,53 @@ If `useIsDefEqBounded` is `true`, we try `isDefEqBounded` before returning false
 -/
 private def canonElemCore (parent : Expr) (f : Expr) (i : Nat) (e : Expr) (useIsDefEqBounded : Bool) : GoalM Expr := do
   let s ← get'
-  if let some c := s.canon.find? e then
+  let key := { f, i, arg := e : CanonArgKey }
+  /-
+  **Note**: We used to use `s.canon.find? e` instead of `s.canonArg.find? key`. This was incorrect.
+  First, for types and implicit arguments, we recursively visit `e` before invoking this function.
+  Thus, `s.canon.find? e` always returns some value `c`, causing us to miss possible canonicalization opportunities.
+  Moreover, `e` may be the argument of two different `f` functions.
+  -/
+  if let some c := s.canonArg.find? key then
     return c
-  let key := (f, i)
-  let eType ← inferType e
-  let cs := s.argMap.find? key |>.getD []
-  for (c, cType) in cs do
-    /-
-    We first check the types
-    The following checks are a performance bottleneck.
-    For example, in the test `grind_ite.lean`, there are many checks of the form:
-    ```
-    w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
-    ```
-    where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
-    -/
-    if (← isDefEqD eType cType) then
-      if (← isDefEq e c) then
-        -- We used to check `c.fvarsSubset e` because it is not
-        -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
-        -- However, we don't revert previously canonicalized elements in the `grind` tactic.
-        -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
-        -- and different locals are added in different branches.
-        modify' fun s => { s with canon := s.canon.insert e c }
-        trace_goal[grind.debug.canon] "found {e} ===> {c}"
-        return c
-      if useIsDefEqBounded then
-        -- If `e` and `c` are not types, we use `isDefEqBounded`
-        if (← isDefEqBounded e c parent) then
+  let c ← go
+  modify' fun s => { s with canonArg := s.canonArg.insert key c }
+  return c
+where
+  go : GoalM Expr := do
+    let s ← get'
+    let key := (f, i)
+    let eType ← inferType e
+    let cs := s.argMap.find? key |>.getD []
+    for (c, cType) in cs do
+      /-
+      We first check the types
+      The following checks are a performance bottleneck.
+      For example, in the test `grind_ite.lean`, there are many checks of the form:
+      ```
+      w_4 ∈ assign.insert v true → Prop =?= w_1 ∈ assign.insert v false → Prop
+      ```
+      where `grind` unfolds the definition of `DHashMap.insert` and `TreeMap.insert`.
+      -/
+      if (← isDefEqD eType cType) then
+        if (← isDefEq e c) then
+          -- We used to check `c.fvarsSubset e` because it is not
+          -- in general safe to replace `e` with `c` if `c` has more free variables than `e`.
+          -- However, we don't revert previously canonicalized elements in the `grind` tactic.
+          -- Moreover, we store the canonicalizer state in the `Goal` because we case-split
+          -- and different locals are added in different branches.
           modify' fun s => { s with canon := s.canon.insert e c }
-          trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+          trace_goal[grind.debug.canon] "found {e} ===> {c}"
           return c
-  trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
-  modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
-  return e
+        if useIsDefEqBounded then
+          -- If `e` and `c` are not types, we use `isDefEqBounded`
+          if (← isDefEqBounded e c parent) then
+            modify' fun s => { s with canon := s.canon.insert e c }
+            trace_goal[grind.debug.canon] "found using `isDefEqBounded`: {e} ===> {c}"
+            return c
+    trace_goal[grind.debug.canon] "({f}, {i}) ↦ {e}"
+    modify' fun s => { s with canon := s.canon.insert e e, argMap := s.argMap.insert key ((e, eType)::cs) }
+    return e
 
 private abbrev canonType (parent f : Expr) (i : Nat) (e : Expr) := withDefault <| canonElemCore parent f i e (useIsDefEqBounded := false)
 private abbrev canonInst (parent f : Expr) (i : Nat) (e : Expr) := withReducibleAndInstances <| canonElemCore parent f i e (useIsDefEqBounded := true)
@@ -159,6 +172,14 @@ private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : Meta
   else
     return .visit
 
+/--
+Returns `true` if `shouldCannon pinfos i arg` is not `.visit`.
+This is a helper function used to implement mbtc.
+-/
+def isSupport (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM Bool := do
+  let r ← shouldCanon pinfos i arg
+  return !r matches .visit
+
 /--
 Auxiliary function for normalizing the arguments of `OfNat.ofNat` during canonicalization.
 This is needed because satellite solvers create `Nat` and `Int` numerals using the

src/Lean/Meta/Tactic/Grind/Cases.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Cases
-
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Types that `grind` will case-split on. -/

src/Lean/Meta/Tactic/Grind/CasesMatch.lean

@@ -7,6 +7,7 @@ module
 prelude
 public import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Cases
 import Lean.Meta.Match.MatcherApp
 import Lean.Meta.Tactic.Grind.MatchCond

src/Lean/Meta/Tactic/Grind/CastLike.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Expr
+import Init.Grind.ToInt
+import Init.Grind.Ring.Envelope
+import Init.Grind.Module.Envelope
+namespace Lean.Meta.Grind
+
+/-- Returns `true` if `declName` is the name of a cast-like function used to implement `grind` solvers -/
+public def isCastLikeDeclName (declName : Name) : Bool :=
+  declName == ``Grind.Ring.OfSemiring.toQ ||
+  declName == ``Grind.IntModule.OfNatModule.toQ ||
+  declName == ``Grind.ToInt.toInt ||
+  declName == ``NatCast.natCast ||
+  declName == ``IntCast.intCast
+
+/-- Returns `true` if `f` is a cast-like operation. -/
+public def isCastLikeFn (f : Expr) : Bool := Id.run do
+  let .const declName _ := f | return false
+  return isCastLikeDeclName declName
+
+public def isCastLikeApp (e : Expr) : Bool :=
+  isCastLikeFn e.getAppFn
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -4,21 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Lean.Meta.LitValues
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Inv
-public import Lean.Meta.Tactic.Grind.PP
-public import Lean.Meta.Tactic.Grind.Ctor
-public import Lean.Meta.Tactic.Grind.Util
-public import Lean.Meta.Tactic.Grind.Beta
-public import Lean.Meta.Tactic.Grind.Internalize
-public import Lean.Meta.Tactic.Grind.Simp
-
+import Init.Grind.Util
+import Lean.Meta.LitValues
+import Lean.Meta.Tactic.Grind.Inv
+import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Ctor
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.Beta
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Internalize
 public section
-
 namespace Lean.Meta.Grind
 
 /--

src/Lean/Meta/Tactic/Grind/Ctor.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp

src/Lean/Meta/Tactic/Grind/Diseq.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Lemmas
 public section
-
 namespace Lean.Meta.Grind
 
 private def dummyEq : Expr := mkApp (mkConst ``Eq [1]) default

src/Lean/Meta/Tactic/Grind/EMatch.lean

@@ -8,9 +8,11 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Util.CollectLevelMVars
 import Lean.Meta.Tactic.Grind.Core
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Simp
 public section
 namespace Lean.Meta.Grind
 namespace EMatch

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -5,16 +5,16 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.Tactics
-public import Lean.HeadIndex
-public import Lean.Util.FoldConsts
-public import Lean.Util.CollectFVars
 public import Lean.Meta.Basic
-public import Lean.Meta.InferType
-public import Lean.Meta.Eqns
-public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Theorems
+import Init.Grind.Util
+import Init.Grind.Tactics
+import Lean.Util.FoldConsts
+import Lean.Util.CollectFVars
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+import Lean.Meta.Eqns
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Message
 import Lean.Meta.Tactic.FVarSubst
 import Lean.Meta.Match.Basic
@@ -312,25 +312,31 @@ def EMatchTheoremKind.isDefault : EMatchTheoremKind → Bool
   | .default _ => true
   | _ => false
 
-def EMatchTheoremKind.toAttributeCore : EMatchTheoremKind → String
-  | .eqLhs true     => " = gen"
-  | .eqLhs false    => " ="
-  | .eqRhs true     => " =_ gen"
-  | .eqRhs false    => " =_"
-  | .eqBoth false   => " _=_"
-  | .eqBoth true    => " _=_ gen"
-  | .eqBwd          => " ←="
-  | .fwd            => " →"
-  | .bwd false      => " ←"
-  | .bwd true       => " ← gen"
-  | .leftRight      => " =>"
-  | .rightLeft      => " <="
-  | .default false  => ""
-  | .default true   => " gen"
+def EMatchTheoremKind.toAttributeCore (kind : EMatchTheoremKind) : String :=
+  match kind with
+  | .eqLhs true     => "= gen"
+  | .eqLhs false    => "="
+  | .eqRhs true     => "=_ gen"
+  | .eqRhs false    => "=_"
+  | .eqBoth false   => "_=_"
+  | .eqBoth true    => "_=_ gen"
+  | .eqBwd          => "←="
+  | .fwd            => "→"
+  | .bwd false      => "←"
+  | .bwd true       => "← gen"
+  | .leftRight      => "=>"
+  | .rightLeft      => "<="
+  | .default false  => "."
+  | .default true   => ". gen"
   | .user           => ""
 
-def EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) : String :=
-  s!"[grind{toAttributeCore k}]"
+def EMatchTheoremKind.toAttribute (k : EMatchTheoremKind) (minIndexable : Bool): String :=
+  if k matches .user then
+    "[grind]"
+  else if minIndexable then
+    s!"[grind! {toAttributeCore k}]"
+  else
+    s!"[grind {toAttributeCore k}]"
 
 private def EMatchTheoremKind.explainFailure : EMatchTheoremKind → String
   | .eqLhs _   => "failed to find pattern in the left-hand side of the theorem's conclusion"
@@ -1302,7 +1308,7 @@ where
 def mkEMatchTheoremForDecl (declName : Name) (thmKind : EMatchTheoremKind) (prios : SymbolPriorities)
     (showInfo := false) (minIndexable := false) : MetaM EMatchTheorem := do
   let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind prios (showInfo := showInfo) (minIndexable := minIndexable)
-    | throwError "`@{thmKind.toAttribute} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
+    | throwError "`@{thmKind.toAttribute minIndexable} theorem {.ofConstName declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
   return thm
 
 def mkEMatchEqTheoremsForDef? (declName : Name) (showInfo := false) : MetaM (Option (Array EMatchTheorem)) := do
@@ -1318,7 +1324,7 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
       throwError "`{.ofConstName declName}` is a definition, you must only use the left-hand side for extracting patterns"
     thms.forM (ematchTheoremsExt.add · attrKind)
   else
-    throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
+    throwError s!"`{thmKind.toAttribute false}` attribute can only be applied to equational theorems or function definitions"
 
 def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
   let throwErr {α} : MetaM α :=
@@ -1369,29 +1375,128 @@ private structure SelectM.State where
 
 private abbrev SelectM := StateT SelectM.State MetaM
 
-private def save (thm : EMatchTheorem) (minIndexable : Bool) : SelectM Unit := do
+def EMatchTheoremKind.toSyntax (kind : EMatchTheoremKind) : CoreM (TSyntax ``Parser.Attr.grindMod) :=
+  match kind with
+  | .eqLhs true     => `(Parser.Attr.grindMod| = gen)
+  | .eqLhs false    => `(Parser.Attr.grindMod|=)
+  | .eqRhs true     => `(Parser.Attr.grindMod|=_ gen)
+  | .eqRhs false    => `(Parser.Attr.grindMod|=_)
+  | .eqBoth false   => `(Parser.Attr.grindMod|_=_)
+  | .eqBoth true    => `(Parser.Attr.grindMod|_=_ gen)
+  | .eqBwd          => `(Parser.Attr.grindMod|←=)
+  | .fwd            => `(Parser.Attr.grindMod|→)
+  | .bwd false      => `(Parser.Attr.grindMod|←)
+  | .bwd true       => `(Parser.Attr.grindMod|← gen)
+  | .leftRight      => `(Parser.Attr.grindMod|=>)
+  | .rightLeft      => `(Parser.Attr.grindMod|<=)
+  | .default false  => `(Parser.Attr.grindMod|.)
+  | .default true   => `(Parser.Attr.grindMod|. gen)
+  | .user           => throwError "`grind` theorem kind is not a modifier"
+
+private def save (ref : Syntax) (thm : EMatchTheorem) (isParam : Bool) (minIndexable : Bool) : SelectM Unit := do
   -- We only save `thm` if the pattern is different from the ones that were already found.
   if (← get).thms.all fun thm' => thm.patterns != thm'.patterns then
-    let baseAttr := if minIndexable then "grind!" else "grind"
-    let msg := s!"] for pattern: {← thm.patterns.mapM fun p => (ppPattern p).toString}"
+    let pats ← thm.patterns.mapM fun p => do
+      let pats ← addMessageContextFull (ppPattern p)
+      pats.format
+    let openBracket  := if isParam then "" else "["
+    let closeBracket := if isParam then "" else "]"
+    let msg := s!"{closeBracket} for pattern: {pats}"
+    let suggestion : Tactic.TryThis.SuggestionText ← match isParam, minIndexable with
+      | false, true  => pure <| Tactic.TryThis.SuggestionText.tsyntax (← `(attr|grind! $(← thm.kind.toSyntax)))
+      | false, false => pure <| .tsyntax (← `(attr|grind $(← thm.kind.toSyntax)))
+      | true,  true  => pure <| .tsyntax (← `(Parser.Tactic.grindParam|!$(← thm.kind.toSyntax)$(⟨ref⟩):ident))
+      | true, false  => pure <| .tsyntax (← `(Parser.Tactic.grindParam|$(← thm.kind.toSyntax) $(⟨ref⟩):ident))
     modify fun s => { s with
       thms := s.thms.push thm
       suggestions := s.suggestions.push {
-        suggestion := .string s!"{baseAttr}{thm.kind.toAttributeCore}"
+        suggestion
         -- **Note**: small hack to include brackets in the suggestion
-        preInfo?   := some "["
-        -- **Note**: appears only on the info view.
+        preInfo?   := some openBracket
+        -- **Note**: appears only in the info view.
         postInfo?  := some msg
       }
     }
 
+register_builtin_option grind.param.codeAction : Bool := {
+  defValue := false
+  descr    := "code-action for `grind` parameters"
+}
+
+/-- Helper type for generating suggestions for `grind` parameters -/
+inductive MinIndexableMode where
+  | /-- `minIndexable := true` -/
+    yes
+  | /-- `minIndexable := false` -/
+    no
+  | /--
+    Tries with and without the minimal indexable subexpression condition, if both produce the
+    same pattern, use the one `minIndexable := false` since it is more compact.
+    -/
+    both
+
+/--
+Tries different modifiers, logs info messages with modifiers that worked, but returns just the first one that worked.
+-/
+def mkEMatchTheoremAndSuggest (ref : Syntax) (declName : Name) (prios : SymbolPriorities)
+    (minIndexable : Bool) (isParam : Bool := false) : MetaM EMatchTheorem := do
+  let tryModifier (thmKind : EMatchTheoremKind) (minIndexable : MinIndexableMode) : SelectM Unit := do
+    try
+      match minIndexable with
+      | .yes =>
+        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := true)
+        save ref thm (minIndexable := true) (isParam := isParam)
+      | .no =>
+        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := false)
+        save ref thm (minIndexable := false) (isParam := isParam)
+      | .both =>
+        let thm₁ ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := true)
+        let thm₂ ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := false)
+        if thm₁.patterns == thm₂.patterns then
+          -- If both produce the same pattern, we save only `minIndexable := false` since it is more compact
+          save ref thm₂ (minIndexable := false) (isParam := isParam)
+        else
+          save ref thm₁ (minIndexable := true) (isParam := isParam)
+          save ref thm₂ (minIndexable := false) (isParam := isParam)
+    catch _ =>
+      return ()
+  let searchCore (minIndexable : MinIndexableMode) : SelectM Unit := do
+    tryModifier (.default false) minIndexable
+    tryModifier (.bwd false) minIndexable
+    tryModifier .fwd minIndexable
+    tryModifier .rightLeft minIndexable
+    tryModifier .leftRight minIndexable
+  let search : SelectM Unit := do
+    if minIndexable then
+      searchCore .yes
+    else if isParam then
+      searchCore .both
+      tryModifier (.eqLhs false) .no
+      tryModifier (.eqRhs false) .no
+    else
+      tryModifier (.eqLhs false) .no
+      tryModifier (.eqRhs false) .no
+      searchCore .no
+      searchCore .yes
+  let (_, s) ← search.run {}
+  if h₁ : 0 < s.thms.size then
+    if !isParam || grind.param.codeAction.get (← getOptions) then
+      if s.suggestions.size == 1 then
+        Tactic.TryThis.addSuggestion ref s.suggestions[0]!
+      else
+        Tactic.TryThis.addSuggestions ref s.suggestions
+    return s.thms[0]
+  else
+    throwError "invalid `grind` theorem, failed to find an usable pattern using different modifiers"
+
 /--
 Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked.
 
 Remark: if `backward.grind.inferPattern` is `true`, then `.default false` is used.
 The parameter `showInfo` is only taken into account when `backward.grind.inferPattern` is `true`.
 -/
-def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities) (minIndexable : Bool) (showInfo : Bool) : MetaM Unit := do
+def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : AttributeKind) (prios : SymbolPriorities)
+    (minIndexable : Bool) (showInfo : Bool) (isParam : Bool := false) : MetaM Unit := do
   let info ← getConstInfo declName
   if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
     ensureNoMinIndexable minIndexable
@@ -1399,34 +1504,8 @@ def addEMatchAttrAndSuggest (ref : Syntax) (declName : Name) (attrKind : Attribu
   else if backward.grind.inferPattern.get (← getOptions) then
     addEMatchAttr declName attrKind (.default false) prios (minIndexable := minIndexable) (showInfo := showInfo)
   else
-    let tryModifier (thmKind : EMatchTheoremKind) (minIndexable : Bool) : SelectM Unit := do
-      try
-        let thm ← mkEMatchTheoremForDecl declName thmKind prios (showInfo := false) (minIndexable := minIndexable)
-        save thm minIndexable
-      catch _ =>
-        return ()
-    let searchCore (minIndexable : Bool) : SelectM Unit := do
-      tryModifier (.bwd false) minIndexable
-      tryModifier .fwd minIndexable
-      tryModifier .rightLeft minIndexable
-      tryModifier .leftRight minIndexable
-    let search : SelectM Unit := do
-      if minIndexable then
-        searchCore true
-      else
-        tryModifier (.eqLhs false) false
-        tryModifier (.eqRhs false) false
-        searchCore false
-        searchCore true
-    let (_, s) ← search.run {}
-    if h₁ : 0 < s.thms.size then
-      if s.suggestions.size == 1 then
-        Tactic.TryThis.addSuggestion ref s.suggestions[0]!
-      else
-        Tactic.TryThis.addSuggestions ref s.suggestions
-      ematchTheoremsExt.add s.thms[0] attrKind
-    else
-      throwError "invalid `grind` theorem, failed to find an usable pattern using different modifiers"
+    let thm ← mkEMatchTheoremAndSuggest ref declName prios minIndexable isParam
+    ematchTheoremsExt.add thm attrKind
 
 def eraseEMatchAttr (declName : Name) : MetaM Unit := do
   /-

src/Lean/Meta/Tactic/Grind/EqResolution.lean

@@ -4,14 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.AppBuilder
-public import Lean.Meta.MatchUtil
-public import Lean.Util.ForEachExpr
-
+public import Lean.Meta.Basic
+import Lean.Meta.AppBuilder
+import Lean.Meta.MatchUtil
+import Lean.Util.ForEachExpr
 public section
-
 namespace Lean.Meta.Grind
 /-! A basic "equality resolution" procedure. -/
 

src/Lean/Meta/Tactic/Grind/ExprPtr.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Expr
-
 public section
-
 namespace Lean.Meta.Grind
 
 @[inline] def isSameExpr (a b : Expr) : Bool :=

src/Lean/Meta/Tactic/Grind/Ext.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
-
 namespace Lean.Meta.Grind
 /-! Extensionality theorems support. -/
 

src/Lean/Meta/Tactic/Grind/ExtAttr.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Ext
-
 public section
-
 namespace Lean.Meta.Grind
 /-! Grind extensionality attribute to mark which `[ext]` theorems should be used. -/
 

src/Lean/Meta/Tactic/Grind/ForallProp.lean

@@ -7,8 +7,10 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Grind.Propagator
+import Init.Simproc
 import Init.Grind.Lemmas
 import Init.Grind.Norm
+import Lean.Meta.Tactic.Grind.PropagatorAttr
 import Lean.Meta.Tactic.Grind.Propagate
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Simp
@@ -127,23 +129,22 @@ def propagateForallPropDown (e : Expr) : GoalM Unit := do
       let h := mkOfEqTrueCore e (← mkEqTrueProof e)
       let h' := mkApp h' h
       addNewRawFact h' e' (← getGeneration e) (.forallProp e)
+    if b.hasLooseBVars then
+      unless (← isProp a) do
+        /-
+        We used to waste a lot of time trying to process terms such as
+        ```
+        ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
+        ```
+        as E-matching theorems. They are "dependent" implications, and should be handled
+        by `propagateForallPropUp`.
+        -/
+        addLocalEMatchTheorems e
     else
-      if b.hasLooseBVars then
-        unless (← isProp a) do
-          /-
-          We used to waste a lot of time trying to process terms such as
-          ```
-          ∀ (h : i + 1 ≤ w), x.abs.getLsbD i = x.abs[i]
-          ```
-          as E-matching theorems. They are "dependent" implications, and should be handled
-          by `propagateForallPropUp`.
-          -/
-          addLocalEMatchTheorems e
-      else
-        unless (← alreadyInternalized b) do return ()
-        if (← isEqFalse b <&&> isProp a) then
-        -- (a → b) = True → b = False → a = False
-        pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
+      unless (← alreadyInternalized b) do return ()
+      if (← isEqFalse b <&&> isProp a) then
+      -- (a → b) = True → b = False → a = False
+      pushEqFalse a <| mkApp4 (mkConst ``Grind.eq_false_of_imp_eq_true) a b (← mkEqTrueProof e) (← mkEqFalseProof b)
 
 builtin_grind_propagator propagateExistsDown ↓Exists := fun e => do
   if (← isEqFalse e) then

src/Lean/Meta/Tactic/Grind/Injection.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Meta.CtorRecognizer
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Clear
+public import Lean.Meta.Basic
+import Lean.Meta.CtorRecognizer
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Clear
 import Lean.Meta.AppBuilder
 
 public section

src/Lean/Meta/Tactic/Grind/Injective.lean

@@ -5,11 +5,13 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.Tactic.Grind.Theorems
+public import Lean.Meta.Tactic.Grind.EMatchTheorem
+import Lean.Meta.FunInfo
 public section
 namespace Lean.Meta.Grind
 
 builtin_initialize registerTraceClass `grind.inj
+builtin_initialize registerTraceClass `grind.inj.assert
 builtin_initialize registerTraceClass `grind.debug.inj
 
 /-- A theorem marked with `@[grind inj]` -/
@@ -37,16 +39,35 @@ private builtin_initialize injectiveTheoremsExt : SimpleScopedEnvExtension Injec
       initial  := {}
     }
 
-private def getSymbols (proof : Expr) : MetaM (List HeadIndex) := do
+private partial def getSymbols (proof : Expr) (hasUniverses : Bool) : MetaM (List HeadIndex) := do
   let type ← inferType proof
-  forallTelescope type fun _ type => do
+  forallTelescope type fun xs type => do
     unless type.isAppOfArity ``Function.Injective 3 do
       throwError "invalid `[grind inj]` theorem, resulting type is not of the form `Function.Injective <fun>`{indentExpr type}"
-    let f := type.appArg!
-    let cs : NameSet := f.foldConsts (init := {}) fun declName s => s.insert declName
+    if xs.isEmpty && hasUniverses then
+      throwError "invalid `[grind inj]` theorem, theorem has universe levels, but no hypotheses{indentExpr type}"
+    let f := type.appArg!.eta
+    let cs ← collectFnNames f
     if cs.isEmpty then
-      throwError "invalid `[grind inj]` theorem, injective function must use at least one constant symbol{indentExpr f}"
+      throwError "invalid `[grind inj]` theorem, injective function must use at least one constant function symbol{indentExpr f}"
     return cs.toList.map (.const ·)
+where
+  collectFnNames (f : Expr) : MetaM NameSet := do
+    if let .const declName _ := f then
+      return { declName }
+    else
+      Prod.snd <$> (go f |>.run {})
+
+  go (e : Expr) : StateRefT NameSet MetaM Unit := do
+    if e.isApp then e.withApp fun f args => do
+      if let .const declName _ := f then
+        modify (·.insert declName)
+      let kinds ← NormalizePattern.getPatternArgKinds f args.size
+      for h : i in *...args.size do
+        let arg  := args[i]
+        let kind := kinds[i]?.getD .relevant
+        if kind matches .relevant | .typeFormer then
+          go arg
 
 private def symbolsToNames (s : List HeadIndex) : List Name :=
   s.map fun
@@ -54,8 +75,9 @@ private def symbolsToNames (s : List HeadIndex) : List Name :=
     | _ => Name.anonymous
 
 def mkInjectiveTheorem (declName : Name) : MetaM InjectiveTheorem := do
+  let info ← getConstInfo declName
   let proof ← getProofForDecl declName
-  let symbols ← getSymbols proof
+  let symbols ← getSymbols proof !info.levelParams.isEmpty
   trace[grind.inj] "{declName}: {symbolsToNames symbols}"
   return {
     levelParams := #[]

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -5,9 +5,10 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.Lemmas
-public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
+import Init.Grind.Util
+import Init.Grind.Lemmas
 import Lean.Meta.LitValues
 import Lean.Meta.Match.MatcherInfo
 import Lean.Meta.Match.MatchEqsExt
@@ -18,6 +19,7 @@ import Lean.Meta.Tactic.Grind.Beta
 import Lean.Meta.Tactic.Grind.MatchCond
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
+import Lean.Meta.Tactic.Grind.PropagateInj
 public section
 namespace Lean.Meta.Grind
 
@@ -235,22 +237,65 @@ private def addMatchEqns (f : Expr) (generation : Nat) : GoalM Unit := do
     -- We disable pattern normalization to prevent the `match`-expression to be reduced.
     activateTheorem (← mkEMatchEqTheorem eqn (normalizePattern := false)) generation
 
-private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
-  if let some (thms, thmMap) := (← get).ematch.thmMap.retrieve? fName then
-    modify fun s => { s with ematch.thmMap := thmMap }
+@[specialize]
+private def activateTheoremsCore [TheoremLike α] (declName : Name)
+    (getThms : GoalM (Theorems α))
+    (setThms : Theorems α → GoalM Unit)
+    (reinsertThm : α → GoalM Unit)
+    (activateThm : α → GoalM Unit) : GoalM Unit := do
+  if let some (thms, s) := (← getThms).retrieve? declName then
+    setThms s
     for thm in thms do
-      trace_goal[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
-      unless (← get).ematch.thmMap.isErased thm.origin do
-        let appMap := (← get).appMap
-        let symbols := thm.symbols.filter fun sym => !appMap.contains sym
-        let thm := { thm with symbols }
+      let origin := TheoremLike.getOrigin thm
+      trace_goal[grind.debug.theorem.activate] "`{declName}` => `{origin.key}`"
+      unless s.isErased origin do
+        let appMap  := (← get).appMap
+        let symbols := TheoremLike.getSymbols thm
+        let symbols := symbols.filter fun sym => !appMap.contains sym
+        let thm     := TheoremLike.setSymbols thm symbols
         match symbols with
         | [] =>
-          trace_goal[grind.debug.ematch.activate] "`{thm.origin.key}`"
-          activateTheorem thm generation
+          trace_goal[grind.debug.theorem.activate] "`{origin.key}`"
+          activateThm thm
         | _ =>
-          trace_goal[grind.debug.ematch.activate] "reinsert `{thm.origin.key}`"
-          modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm }
+          trace_goal[grind.debug.theorem.activate] "reinsert `{origin.key}`"
+          reinsertThm thm
+
+private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
+  activateTheoremsCore fName (return (← get).ematch.thmMap)
+    (fun thmMap => modify fun s => { s with ematch.thmMap := thmMap })
+    (fun thm => modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm })
+    (fun thm => activateTheorem thm generation)
+
+private def mkEMatchTheoremWithKind'? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : EMatchTheoremKind)
+    (symPrios : SymbolPriorities) : MetaM (Option EMatchTheorem) := do
+  try
+    mkEMatchTheoremWithKind? origin levelParams proof kind symPrios (minIndexable := true)
+  catch _ =>
+    return none
+
+private def activateInjectiveTheorem (injThm : InjectiveTheorem) (generation : Nat) : GoalM Unit := do
+  let type ← inferType injThm.proof
+  if type.isForall then
+    let symPrios ← getSymbolPriorities
+    let thm? ← mkEMatchTheoremWithKind'? injThm.origin injThm.levelParams injThm.proof .fwd symPrios
+      <||>
+      mkEMatchTheoremWithKind'? injThm.origin injThm.levelParams injThm.proof (.default false) symPrios
+    let some thm := thm? | reportIssue! "failed to assert injectivity theorem `{injThm.origin.pp}`"
+    activateTheorem thm generation
+  else
+    addNewRawFact injThm.proof type generation (.inj injThm.origin)
+
+private def activateInjectiveTheorems (declName : Name) (generation : Nat) : GoalM Unit := do
+  if (← getConfig).inj then
+    activateTheoremsCore declName (return (← get).inj.thms)
+      (fun thms => modify fun s => { s with inj.thms := thms })
+      (fun thm => modify fun s => { s with inj.thms := s.inj.thms.insert thm })
+      (fun thm => activateInjectiveTheorem thm generation)
+
+private def activateTheorems (declName : Name) (generation : Nat) : GoalM Unit := do
+  activateTheoremPatterns declName generation
+  activateInjectiveTheorems declName generation
 
 /--
 If type of `a` is a structure and is tagged with `[grind ext]` attribute,
@@ -380,7 +425,13 @@ where
     trace_goal[grind.internalize] "[{generation}] {e}"
     match e with
     | .bvar .. => unreachable!
-    | .sort .. => return ()
+    | .sort .. =>
+      /-
+      **Note**: It may seem wasteful to create ENodes for sorts, but it is useful for the E-matching module.
+      The E-matching module assumes that the arguments of an internalized application have also been internalized,
+      unless they are `grind` gadgets.
+      -/
+      mkENode' e generation
     | .fvar .. =>
       mkENode' e generation
       checkAndAddSplitCandidate e
@@ -405,7 +456,7 @@ where
       mkENode e generation
     | .const declName _ =>
       mkENode e generation
-      activateTheoremPatterns declName generation
+      activateTheorems declName generation
     | .mvar .. =>
       if (← reportMVarInternalization) then
         reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
@@ -448,7 +499,7 @@ where
           registerParent e c
         else
           if let .const fName _ := f then
-            activateTheoremPatterns fName generation
+            activateTheorems fName generation
           else
             internalizeImpl f generation e
           registerParent e f
@@ -460,5 +511,6 @@ where
         Solvers.internalize e parent?
         propagateUp e
         propagateBetaForNewApp e
+        mkInjEq e
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Intro.lean

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Injection

src/Lean/Meta/Tactic/Grind/Inv.lean

@@ -6,8 +6,10 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Util
 import Lean.Meta.Tactic.Grind.Proof
 import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.Util
 namespace Lean.Meta.Grind
 /-!
 Debugging support code for checking basic invariants.

src/Lean/Meta/Tactic/Grind/LawfulEqCmp.lean

@@ -4,23 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Tactic.Grind.SynthInstance
 public section
-
+namespace Lean.Meta.Grind
 /-!
 Support for type class `LawfulEqCmp`.
 -/
 /-
-Note: we will have similar support for `Associative` and `Commutative`. In the future, we should have
+**Note**: we will have similar support for `Associative` and `Commutative`. In the future, we should have
 a mechanism for letting users to install their own handlers.
 -/
 
-namespace Lean.Meta.Grind
-
 /--
 If `op` implements `LawfulEqCmp`, then returns the proof term for
 `∀ a b, op a b = .eq → a = b`

src/Lean/Meta/Tactic/Grind/MBTC.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Canon
+import Lean.Meta.Tactic.Grind.CastLike
 public section
 namespace Lean.Meta.Grind
 
@@ -36,7 +38,40 @@ private structure ArgInfo where
   arg : Expr
   app : Expr
 
-private abbrev Map := Std.HashMap (Expr × Nat) (List ArgInfo)
+/-- Key for detecting pairs of terms to case-split on. -/
+private structure Key where
+  /--
+  Mask constructed using the application a term occurs in. It includes
+  the function and support arguments.
+  We use two auxiliary "fake" terms to create the mask `_main` and `_other`.
+  Example suppose we have the application `@Prod.mk Bool Nat flag n`, and we
+  are trying to create a key for `n` at this application. The mask will be
+  ```
+  @Prod.mk Bool Nat _other _main
+  ```
+  We define "support" in this module as terms using the canonicalizer `isSupport`
+  function.
+  -/
+  mask : Expr
+  deriving BEq, Hashable
+
+private def mainMark  := mkConst `__grind_main_arg
+private def otherMark := mkConst `__grind_other_arg
+
+private def mkKey (e : Expr) (i : Nat) : MetaM Key :=
+  e.withApp fun f args => do
+    let info ← getFunInfo f
+    let mut args := Array.toVector args
+    for h : j in *...args.size do
+      let arg := args[j]
+      if i == j then
+        args := args.set j mainMark
+      else if !(← Canon.isSupport info.paramInfo j arg) then
+        args := args.set j otherMark
+    let mask := mkAppN f args.toArray
+    return { mask }
+
+private abbrev Map := Std.HashMap Key (List ArgInfo)
 private abbrev Candidates := Std.HashSet SplitInfo
 private def mkCandidate (a b : ArgInfo) (i : Nat) : GoalM SplitInfo := do
   let (lhs, rhs) := if a.arg.lt b.arg then
@@ -65,25 +100,27 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
     unless (← ctx.isInterpreted e) do
       let f := e.getAppFn
       /-
-      Remark: we ignore type class instances in model-based theory combination.
+      Remark: we ignore type class instances and cast-like applications in model-based theory combination.
       `grind` treats instances as support elements, and they are handled by the canonicalizer.
+      cast-like internal operations and handled by their associated solver.
       -/
-      unless (← isFnInstance f) do
+      if !(← isFnInstance f) && !isCastLikeFn f then
         let mut i := 0
         for arg in e.getAppArgs do
           let some arg ← getRoot? arg | pure ()
           if (← ctx.hasTheoryVar arg) then
             trace[grind.debug.mbtc] "{arg} @ {f}:{i}"
             let argInfo : ArgInfo := { arg, app := e }
-            if let some otherInfos := map[(f, i)]? then
+            let key ← mkKey e i
+            if let some otherInfos := map[key]? then
               unless otherInfos.any fun info => isSameExpr arg info.arg do
                 for otherInfo in otherInfos do
                   if (← ctx.eqAssignment arg otherInfo.arg) then
                     if (← hasSameType arg otherInfo.arg) then
                       candidates := candidates.insert (← mkCandidate argInfo otherInfo i)
-                map := map.insert (f, i) (argInfo :: otherInfos)
+                map := map.insert key (argInfo :: otherInfos)
             else
-              map := map.insert (f, i) [argInfo]
+              map := map.insert key [argInfo]
           i := i + 1
   if candidates.isEmpty then
     return false
@@ -95,6 +132,7 @@ def mbtc (ctx : MBTC.Context) : GoalM Bool := do
     if (← isKnownCaseSplit info) then
       return none
     let .arg a b _ eq _ := info | return none
+    trace[grind.mbtc] "{eq}"
     internalize eq (Nat.max (← getGeneration a) (← getGeneration b))
     return some info
   if result.isEmpty then

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -8,8 +8,10 @@ prelude
 public import Lean.Meta.Tactic.Util
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Lemmas
+import Lean.PrettyPrinter
 import Lean.Meta.Tactic.ExposeNames
 import Lean.Meta.Tactic.Simp.Diagnostics
+import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Meta.Tactic.Grind.PropagatorAttr
@@ -20,6 +22,7 @@ import Lean.Meta.Tactic.Grind.Inv
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.Solve
+import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.Cases
 import Lean.Meta.Tactic.Grind.LawfulEqCmp

src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean

@@ -4,19 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Lean.Util.PtrSet
-public import Lean.Meta.Transform
-public import Lean.Meta.Basic
-public import Lean.Meta.InferType
-public import Lean.Meta.Tactic.Grind.ExprPtr
-public import Lean.Meta.Tactic.Grind.Util
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Util
+import Lean.Util.PtrSet
+import Lean.Meta.Transform
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+import Lean.Meta.Tactic.Grind.ExprPtr
+import Lean.Meta.Tactic.Grind.Util
 public section
-
 namespace Lean.Meta.Grind
 
 private abbrev M := StateRefT (Std.HashMap ExprPtr Expr) GrindM

src/Lean/Meta/Tactic/Grind/MatchCond.lean

@@ -4,16 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind
-public import Init.Simproc
-public import Lean.Meta.Tactic.Contradiction
-public import Lean.Meta.Tactic.Grind.ProveEq
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind
+import Init.Simproc
+import Lean.Meta.Tactic.Contradiction
+import Lean.Meta.Tactic.Grind.ProveEq
+import Lean.Meta.Tactic.Grind.PropagatorAttr
 public section
-
 namespace Lean.Meta.Grind
 /-
 Remark: the `simp` module has some support for `MatchCond`, but it is

src/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean

@@ -4,15 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Util
-public import Init.Simproc
 public import Lean.Meta.Tactic.Simp.Simproc
-public import Lean.Meta.Tactic.Simp.Rewrite
-
+import Init.Grind.Util
+import Init.Simproc
+import Lean.Meta.Tactic.Simp.Rewrite
 public section
-
 namespace Lean.Meta.Grind
 /--
 Returns `Grind.simpMatchDiscrsOnly e`. Recall that `Grind.simpMatchDiscrsOnly` is

src/Lean/Meta/Tactic/Grind/PP.lean

@@ -5,15 +5,18 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Util
-public import Init.Grind.PP
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Arith.Model
-public import Lean.Meta.Tactic.Grind.Arith.Offset.Types
-public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
-public import Lean.Meta.Tactic.Grind.Arith.Linear.PP
-public import Lean.Meta.Tactic.Grind.AC.PP
+import Init.Grind.Util
+import Init.Grind.Injective
+import Init.Grind.PP
+import Lean.Meta.Tactic.Grind.Arith.Model
+import Lean.Meta.Tactic.Grind.Arith.Offset.Types
+import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+import Lean.Meta.Tactic.Grind.Arith.Linear.PP
+import Lean.Meta.Tactic.Grind.AC.PP
+import Lean.Meta.Tactic.Grind.CastLike
 import Lean.PrettyPrinter
+import Lean.Meta.CtorRecognizer
 public section
 
 namespace Lean.Meta.Grind
@@ -88,9 +91,72 @@ def ppExprArray (cls : Name) (header : String) (es : Array Expr) (clsElem : Name
   let es := es.map (toTraceElem · clsElem)
   .trace { cls } header es
 
+section EqcFilter
+/-!
+Functions for deciding whether an expression is a support application or not
+when displaying equivalence classes.
+This is hard-coded for now. We will probably make it extensible in the future.
+-/
+private def isGadget (declName : Name) : Bool :=
+  declName == ``Grind.nestedDecidable || declName == ``Grind.leftInv
+
+private def isBuiltin (declName : Name) : Bool :=
+  declName == ``ite || declName == ``dite || declName == ``cast
+
+/-- Result for helper function `isArithOfCastLike` -/
+private inductive Result where
+  | num | cast | no
+  deriving Inhabited
+
+@[macro_inline] private def Result.and : Result → Result → Result
+  | .no,   _ | _, .no   => .no
+  | .cast, _ | _, .cast => .cast
+  | .num, .num => .num
+
+/--
+Returns `true` if `e` is an expression constructed using numerals,
+`grind` cast-like operations, and arithmetic terms. Moreover, the
+expression contains at least one cast-like application.
+This kind of term is constructed by `grind` satellite solvers.
+-/
+private partial def isArithOfCastLike (e : Expr) : Bool :=
+  go e matches .cast
+where
+  go (e : Expr) : Result :=
+    match_expr e with
+    | HAdd.hAdd _ _ _ _ a b => go a |>.and (go b)
+    | HSub.hSub _ _ _ _ a b => go a |>.and (go b)
+    | HMul.hMul _ _ _ _ a b => go a |>.and (go b)
+    | HDiv.hDiv _ _ _ _ a b => go a |>.and (go b)
+    | HMod.hMod _ _ _ _ a b => go a |>.and (go b)
+    | HPow.hPow _ _ _ _ a _ => go a
+    | Neg.neg _ _ a         => go a
+    | OfNat.ofNat _ _ _     => .num
+    | _ => if isCastLikeApp e then .cast else .no
+
+/--
+Returns `true` if `e` is a support-like application.
+Recall that equivalence classes that contain only support applications are displayed in the "others" category.
+-/
+private def isSupportApp (e : Expr) : MetaM Bool := do
+  if isArithOfCastLike e then return true
+  let .const declName _ := e.getAppFn | return false
+  -- Check whether `e` is the projection of a constructor
+  if let some info ← getProjectionFnInfo? declName then
+    if e.getAppNumArgs == info.numParams + 1 then
+      if (← isConstructorApp e.appArg!) then
+        return true
+  return isCastLikeDeclName declName || isGadget declName || isBuiltin declName || isMatcherCore (← getEnv) declName
+
+end EqcFilter
+
+private def ppEqc (eqc : List Expr) (children : Array MessageData := #[]) : MessageData :=
+  .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) children
+
 private def ppEqcs : M Unit := do
    let mut trueEqc?  : Option MessageData := none
    let mut falseEqc? : Option MessageData := none
+   let mut regularEqcs : Array MessageData := #[]
    let mut otherEqcs : Array MessageData := #[]
    let goal ← read
    for eqc in goal.getEqcs (sort := true) do
@@ -105,11 +171,22 @@ private def ppEqcs : M Unit := do
      else if let e :: _ :: _ := eqc then
        -- We may want to add a flag to pretty print equivalence classes of nested proofs
        unless (← isProof e) do
-         otherEqcs := otherEqcs.push <| .trace { cls := `eqc } (.group ("{" ++ (MessageData.joinSep (eqc.map toMessageData) ("," ++ Format.line)) ++  "}")) #[]
+         let mainEqc ← eqc.filterM fun e => return !(← isSupportApp e)
+         if mainEqc.length <= 1 then
+           otherEqcs := otherEqcs.push <| ppEqc eqc
+         else
+           let supportEqc ← eqc.filterM fun e => isSupportApp e
+           if supportEqc.isEmpty then
+             regularEqcs := regularEqcs.push <| ppEqc mainEqc
+           else
+             regularEqcs := regularEqcs.push <| ppEqc mainEqc #[ppEqc supportEqc]
+
+   unless otherEqcs.isEmpty do
+     regularEqcs := regularEqcs.push <| .trace { cls := `eqc } "others" otherEqcs
    if let some trueEqc := trueEqc? then pushMsg trueEqc
    if let some falseEqc := falseEqc? then pushMsg falseEqc
-   unless otherEqcs.isEmpty do
-     pushMsg <| .trace { cls := `eqc } "Equivalence classes" otherEqcs
+   unless regularEqcs.isEmpty do
+     pushMsg <| .trace { cls := `eqc } "Equivalence classes" regularEqcs
 
 private def ppEMatchTheorem (thm : EMatchTheorem) : MetaM MessageData := do
   let m := m!"{thm.origin.pp}: {thm.patterns.map ppPattern}"

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Parser.Command
-
 public section
-
 namespace Lean.Parser.Command
 /-!
 Builtin parsers for `grind` related commands

src/Lean/Meta/Tactic/Grind/Proj.lean

@@ -4,14 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.ProjFns
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.Internalize
-
+import Lean.ProjFns
+import Lean.Meta.Tactic.Grind.Internalize
 public section
-
 namespace Lean.Meta.Grind
 
 /--

src/Lean/Meta/Tactic/Grind/Proof.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind.Lemmas
 public import Lean.Meta.Tactic.Grind.Types
-
+import Init.Grind.Lemmas
 public section
-
 namespace Lean.Meta.Grind
 
 private def isEqProof (h : Expr) : MetaM Bool := do

src/Lean/Meta/Tactic/Grind/Propagate.lean

@@ -5,12 +5,12 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind
-public import Lean.Meta.Tactic.Grind.Proof
-public import Lean.Meta.Tactic.Grind.PropagatorAttr
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.Ext
-public import Lean.Meta.Tactic.Grind.Internalize
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Ext
 import Lean.Meta.Tactic.Grind.Diseq
 public section
 namespace Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/PropagateInj.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+import Init.Grind.Propagator
+import Init.Grind.Injective
+import Lean.Meta.Tactic.Grind.Proof
+import Lean.Meta.Tactic.Grind.PropagatorAttr
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.Injective
+namespace Lean.Meta.Grind
+/--
+If `e` is an application of the form `f a` where `f` is an injective function
+in `(← get).inj.fns`, asserts `f⁻¹ (f a) = a`
+-/
+public def mkInjEq (e : Expr) : GoalM Unit := do
+  let .app f a := e | return ()
+  let some info := (← get).inj.fns.find? { expr := f } | return ()
+  let invApp := mkApp info.inv e
+  internalize invApp (← getGeneration e)
+  trace[grind.inj.assert] "{invApp}, {a}"
+  pushEq invApp a <| mkApp info.heq a
+
+def initInjFn (us : List Level) (α β : Expr) (f : Expr) (h : Expr) : GoalM Unit := do
+  let hidx := f.toHeadIndex
+  let mut first := true
+  for e in (← get).appMap.findD hidx [] do
+    if e.isApp && isSameExpr e.appFn! f then
+      if first then
+        initLeftInv e.appArg!
+        first := false
+      mkInjEq e
+where
+  initLeftInv (a : Expr) : GoalM Unit := do
+    let [u, _] := us | unreachable!
+    let nonEmpty := mkApp2 (mkConst ``Nonempty.intro [u]) α a
+    let inv := mkApp5 (mkConst ``Grind.leftInv us) α β f h nonEmpty
+    let inv ← preprocessLight inv
+    let args := inv.getAppArgs
+    let heq := mkAppN (mkConst ``Grind.leftInv_eq us) args
+    modify fun s => { s with inj.fns := s.inj.fns.insert { expr := f } { inv, heq } }
+
+builtin_grind_propagator propagateInj ↓Function.Injective := fun e => do
+  let_expr i@Function.Injective α β f := e | return ()
+  if (← isEqTrue e) then
+    let f' := f.eta
+    let f ← if isSameExpr f f' then
+      pure f
+    else
+      let f' ← preprocessLight f'
+      internalize f' (← getGeneration e)
+      pure f'
+    initInjFn i.constLevels! α β f (mkOfEqTrueCore e (← mkEqTrueProof e))
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/PropagatorAttr.lean

@@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Grind
 public import Lean.Meta.Tactic.Grind.Proof
-
+import Lean.Compiler.InitAttr
+import Init.Grind
 public section
-
 namespace Lean.Meta.Grind
 
 /-- Builtin propagators. -/

src/Lean/Meta/Tactic/Grind/ProveEq.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Simp
-
 public section
-
 namespace Lean.Meta.Grind
 /--
 If `e` has not been internalized yet, instantiate metavariables, unfold reducible, canonicalize,

src/Lean/Meta/Tactic/Grind/ReflCmp.lean

@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Grind.Types
-public import Lean.Meta.Tactic.Grind.SynthInstance
-
+import Lean.Meta.Tactic.Grind.SynthInstance
+import Lean.Meta.Tactic.Grind.Util
 public section
-
+namespace Lean.Meta.Grind
 /-!
 Support for type class `ReflCmp`.
 -/
@@ -19,8 +18,6 @@ Note: we will have similar support for `Associative` and `Commutative`. In the f
 a mechanism for letting users to install their own handlers.
 -/
 
-namespace Lean.Meta.Grind
-
 /--
 If `op` implements `ReflCmp`, then returns the proof term for
 `∀ a b, a = b → op a b = .eq`

src/Lean/Meta/Tactic/Grind/RevertAll.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Revert
-
 public section
-
 namespace Lean.Meta.Grind
 /--
 Reverts all free variables in the goal `mvarId`.

src/Lean/Meta/Tactic/Grind/SearchM.lean

@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Lean.Util.ForEachExpr
 public import Lean.Meta.Tactic.Grind.Types
-
+import Lean.Util.ForEachExpr
 public section
-
 namespace Lean.Meta.Grind
 /--
 A `choice` (aka backtracking) point in the search tree.

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -4,19 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Tactic.Simp.Simproc
-public import Lean.Meta.Tactic.Grind.Simp
-public import Lean.Meta.Tactic.Grind.MatchDiscrOnly
-public import Lean.Meta.Tactic.Grind.MatchCond
-public import Lean.Meta.Tactic.Grind.ForallProp
-public import Lean.Meta.Tactic.Grind.Arith.Simproc
-public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
-public import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
-
+import Lean.Meta.Tactic.Grind.Simp
+import Lean.Meta.Tactic.Grind.MatchDiscrOnly
+import Lean.Meta.Tactic.Grind.MatchCond
+import Lean.Meta.Tactic.Grind.ForallProp
+import Lean.Meta.Tactic.Grind.Arith.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
+import Lean.Meta.Tactic.Grind.Util
+import Init.Grind.Norm
 public section
-
 namespace Lean.Meta.Grind
 
 builtin_initialize normExt : SimpExtension ← mkSimpExt

src/Lean/Meta/Tactic/Grind/Split.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.SearchM
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.CasesMatch
 import Lean.Meta.Tactic.Grind.Internalize
 public section

src/Lean/Meta/Tactic/Grind/SynthInstance.lean

@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Lean.Meta.SynthInstance
 public import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.SynthInstance
 public section
 namespace Lean.Meta.Grind
 /--

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -5,19 +5,20 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Tactics
-public import Init.Data.Queue
-public import Std.Data.TreeSet.Basic
-public import Lean.HeadIndex
+public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.Simp.Types
-public import Lean.Meta.Tactic.Grind.ExprPtr
 public import Lean.Meta.Tactic.Grind.AlphaShareCommon
 public import Lean.Meta.Tactic.Grind.Attr
-public import Lean.Meta.Tactic.Grind.ExtAttr
-public import Lean.Meta.Tactic.Grind.EMatchTheorem
-meta import Lean.Parser.Do
+public import Init.Data.Queue
+import Lean.Meta.Tactic.Grind.ExprPtr
+import Init.Grind.Tactics
+import Std.Data.TreeSet.Basic
+import Lean.HeadIndex
+import Lean.Meta.Tactic.Grind.ExtAttr
+import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Match.MatchEqsExt
 import Lean.PrettyPrinter
+meta import Lean.Parser.Do
 public section
 namespace Lean.Meta.Grind
 
@@ -82,6 +83,8 @@ inductive SplitSource where
     existsProp (e : Expr)
   | /-- Input goal -/
     input
+  | /-- Injectivity theorem. -/
+    inj (origin : Origin)
   deriving Inhabited
 
 def SplitSource.toMessageData : SplitSource → MessageData
@@ -92,6 +95,7 @@ def SplitSource.toMessageData : SplitSource → MessageData
   | .forallProp e => m!"Forall propagation at{indentExpr e}"
   | .existsProp e => m!"Exists propagation at{indentExpr e}"
   | .input => "Initial goal"
+  | .inj origin => m!"Injectivity {origin.pp}"
 
 /-- Context for `GrindM` monad. -/
 structure Context where
@@ -472,6 +476,7 @@ inductive NewFact where
   | fact (prop proof : Expr) (generation : Nat)
 
 -- This type should be considered opaque outside this module.
+@[expose]  -- for codegen
 def ENodeMap := PHashMap ExprPtr ENode
 instance : Inhabited ENodeMap where
   default := private (id {})  -- TODO(sullrich): `id` works around `private` not respecting the expected type
@@ -599,11 +604,18 @@ structure NewRawFact where
   splitSource  : SplitSource
   deriving Inhabited
 
+structure CanonArgKey where
+  f   : Expr
+  i   : Nat
+  arg : Expr
+  deriving BEq, Hashable
+
 /-- Canonicalizer state. See `Canon.lean` for additional details. -/
 structure Canon.State where
   argMap     : PHashMap (Expr × Nat) (List (Expr × Expr)) := {}
   canon      : PHashMap Expr Expr := {}
   proofCanon : PHashMap Expr Expr := {}
+  canonArg   : PHashMap CanonArgKey Expr := {}
   deriving Inhabited
 
 /-- Trace information for a case split. -/
@@ -747,9 +759,15 @@ structure UnitLike.State where
   map : PHashMap ExprPtr (Option Expr) := {}
   deriving Inhabited
 
+structure InjectiveInfo where
+  inv : Expr
+  heq : Expr
+  deriving Inhabited
+
 /-- State for injective theorem support. -/
 structure Injective.State where
   thms : InjectiveTheorems
+  fns  : PHashMap ExprPtr InjectiveInfo := {}
   deriving Inhabited
 
 /-- The `grind` goal. -/

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -4,18 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
-public import Init.Simproc
-public import Init.Grind.Tactics
-public import Lean.Meta.AbstractNestedProofs
+public import Lean.Meta.Basic
 public import Lean.Meta.Transform
-public import Lean.Meta.Tactic.Util
-public import Lean.Meta.Tactic.Clear
 public import Lean.Meta.Tactic.Simp.Simproc
-
+import Init.Simproc
+import Init.Grind.Tactics
+import Lean.Meta.AbstractNestedProofs
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Clear
 public section
-
 namespace Lean.Meta.Grind
 /--
 Throws an exception if target of the given goal contains metavariables.

src/Lean/Meta/Tactic/Grind/VarRename.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Prelude
 public import Init.Data.Array.QSort
 public import Std.Data.HashSet
 public section

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Try
 public import Lean.Meta.Tactic.LibrarySearch
@@ -13,9 +12,8 @@ public import Lean.Meta.Tactic.Grind.Cases
 public import Lean.Meta.Tactic.Grind.EMatchTheorem
 public import Lean.Meta.Tactic.FunIndInfo
 public import Lean.Meta.Tactic.FunIndCollect
-
+import Lean.Meta.Eqns
 public section
-
 namespace Lean.Meta.Try.Collector
 
 structure InductionCandidate where

src/Lean/Meta/WHNF.lean

@@ -130,10 +130,14 @@ private def mkNullaryCtor (type : Expr) (nparams : Nat) : MetaM (Option Expr) :=
   let (some ctor) ← getFirstCtor d | pure none
   return mkAppN (mkConst ctor lvls) (type.getAppArgs.shrink nparams)
 
-private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : Option RecursorRule :=
+private def getRecRuleFor (recVal : RecursorVal) (major : Expr) : MetaM (Option RecursorRule) := do
   match major.getAppFn with
-  | .const fn _ => recVal.rules.find? fun r => r.ctor == fn
-  | _           => none
+  | .const fn _ =>
+    let .ctorInfo info ← getConstInfo fn | return none
+    let rule := recVal.rules[info.cidx]!
+    assert! rule.ctor == fn
+    return rule
+  | _           => return none
 
 private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
   let majorType ← inferType major
@@ -242,7 +246,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
     major ← major.toCtorIfLit
     major ← cleanupNatOffsetMajor major
     major ← toCtorWhenStructure recVal.getMajorInduct major
-    match getRecRuleFor recVal major with
+    match (← getRecRuleFor recVal major) with
     | some rule =>
       let majorArgs := major.getAppArgs
       if recLvls.length != recVal.levelParams.length then

src/Lean/Parser/Command.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Lean.Parser.Term
 public import Lean.Parser.Do
+import Lean.DocString.Parser
+public import Lean.DocString.Formatter
 meta import Lean.Parser.Basic
 
 public section
@@ -49,6 +51,7 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
+
 /--
 `/-! <text> -/` defines a *module docstring* that can be displayed by documentation generation
 tools. The string is associated with the corresponding position in the file. It can be used
@@ -56,7 +59,8 @@ multiple times in the same file.
 -/
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
-  "/-!" >> commentBody >> ppLine
+  "/-!" >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
+
 
 def namedPrio := leading_parser
   atomic (" (" >> nonReservedSymbol "priority") >> " := " >> withoutPosition priorityParser >> ")"
@@ -889,6 +893,7 @@ builtin_initialize
   register_parser_alias                                                 optDeclSig
   register_parser_alias                                                 openDecl
   register_parser_alias                                                 docComment
+  register_parser_alias                                                 plainDocComment
   register_parser_alias                                                 visibility
 
 /--

src/Lean/Parser/Term.lean

@@ -8,8 +8,13 @@ module
 prelude
 public import Lean.Parser.Attr
 public import Lean.Parser.Level
+public import Lean.Parser.Term.Basic
+public import Lean.Parser.Term.Basic
+meta import Lean.Parser.Term.Basic
 public import Lean.Parser.Term.Doc
 meta import Lean.Parser.Basic
+import Lean.DocString.Parser
+public import Lean.DocString.Formatter
 
 public section
 
@@ -17,6 +22,38 @@ namespace Lean
 namespace Parser
 
 namespace Command
+
+open Lean.Parser in
+def versoCommentBodyFn : ParserFn := fun c s =>
+  let startPos := s.pos
+  let s := finishCommentBlock (pushMissingOnError := true) 1 c s
+  if !s.hasError then
+    let commentEndPos := s.pos
+    let endPos := c.prev (c.prev commentEndPos)
+    let endPos := if endPos ≤ c.inputString.endPos then endPos else c.inputString.endPos
+    let c' := c.setEndPos endPos (by unfold endPos; split <;> simp [*])
+    let s := Doc.Parser.document {} c' (s.setPos startPos)
+    if s.hasError then
+      s.pushSyntax .missing
+    else
+      (rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true)) c s
+  else s
+
+public def versoCommentBody : Parser where
+  fn := nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn
+
+@[combinator_parenthesizer versoCommentBody, expose]
+public def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+
+open PrettyPrinter Formatter in
+open Syntax.MonadTraverser in
+@[combinator_formatter versoCommentBody, expose]
+public def versoCommentBody.formatter : PrettyPrinter.Formatter := do
+  visitArgs $ do
+    visitAtom `«-/»
+    goLeft
+    Lean.Doc.Parser.document.formatter
+
 def commentBody : Parser :=
 { fn := rawFn (finishCommentBlock (pushMissingOnError := true) 1) (trailingWs := true) }
 
@@ -25,86 +62,31 @@ def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinator_formatter commentBody, expose]
 def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
-/-- A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
+/--
+A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
 a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
 
-A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
-example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. -/
+At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
+are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
+`plainDocComment` to always treat the contents as plain text.
+
+A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
+in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
+A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
+-/
 -- @[builtin_doc] -- FIXME: suppress the hover
+@[run_builtin_parser_attribute_hooks]
 def docComment := leading_parser
-  ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
+  ppDedent $ "/--" >> ppSpace >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
+
+@[inherit_doc docComment, run_builtin_parser_attribute_hooks]
+def plainDocComment : Parser := Doc.Parser.withoutVersoSyntax docComment
+
 end Command
 
-builtin_initialize
-  registerBuiltinParserAttribute `builtin_tactic_parser ``Category.tactic .both
-  registerBuiltinDynamicParserAttribute `tactic_parser `tactic
-
-@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
-  categoryParser `tactic rbp
-
-@[inline] def convParser (rbp : Nat := 0) : Parser :=
-  categoryParser `conv rbp
-
-namespace Tactic
-
-/-- `sepByIndentSemicolon(p)` parses a sequence of `p` optionally followed by `;`,
-similar to `manyIndent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
-the `;` is mandatory. This is used by tactic parsing, so that
-```
-example := by
-  skip
-  skip
-```
-is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks, builtin_doc]
-def sepByIndentSemicolon (p : Parser) : Parser :=
-  sepByIndent p "; " (allowTrailingSep := true)
-
-/-- `sepBy1IndentSemicolon(p)` parses a (nonempty) sequence of `p` optionally followed by `;`,
-similar to `many1Indent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
-the `;` is mandatory. This is used by tactic parsing, so that
-```
-example := by
-  skip
-  skip
-```
-is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks, builtin_doc]
-def sepBy1IndentSemicolon (p : Parser) : Parser :=
-  sepBy1Indent p "; " (allowTrailingSep := true)
-
-builtin_initialize
-  register_parser_alias sepByIndentSemicolon
-  register_parser_alias sepBy1IndentSemicolon
-
-@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
-  sepBy1IndentSemicolon tacticParser
-/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
-It runs the tactics in sequence, and fails if the goal is not solved. -/
-@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
-  "{ " >> sepByIndentSemicolon tacticParser >> ppDedent ppLine >> "}"
-
-/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
-Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
-@[builtin_doc] def tacticSeq := leading_parser
-  tacticSeqBracketed <|> tacticSeq1Indented
-
-/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
-The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
-position set. -/
-@[builtin_doc] def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
-  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
-
-/- Raw sequence for quotation and grouping -/
-def seq1 :=
-  node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true)
-
-end Tactic
-
 def darrow : Parser := " => "
 def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
 
-
 namespace Term
 
 /-! # Built-in parsers -/
@@ -148,81 +130,8 @@ def optSemicolon (p : Parser) : Parser :=
 Every proposition is propositionally equal to either `True` or `False`. -/
 @[builtin_term_parser] def prop := leading_parser
   "Prop"
-/--
-A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
-For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.
 
-The way this works is that holes create fresh metavariables.
-The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
-This is often known as *unification*.
 
-Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
-* In `match` patterns, holes are catch-all patterns.
-* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.
-
-Related concept: implicit parameters are automatically filled in with holes during the elaboration process.
-
-See also `?m` syntax (synthetic holes).
--/
-@[builtin_term_parser] def hole := leading_parser
-  "_"
-/--
-A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should be synthesized using tactics.
-- `?_` creates a fresh metavariable with an auto-generated name.
-- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.
-
-In particular, the synthetic hole syntax creates "synthetic opaque metavariables",
-the same kind of metavariable used to represent goals in the tactic state.
-
-Synthetic holes are similar to holes in that `_` also creates metavariables,
-but synthetic opaque metavariables have some different properties:
-- In tactics such as `refine`, only synthetic holes yield new goals.
-- During elaboration, unification will not solve for synthetic opaque metavariables, they are "opaque".
-  This is to prevent counterintuitive behavior such as disappearing goals.
-- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
-
-## Delayed assigned metavariables
-
-This section gives an overview of some technical details of synthetic holes, which you should feel free to skip.
-Understanding delayed assignments is mainly useful for those who are working on tactics and other metaprogramming.
-It is included here until there is a suitable place for it in the reference manual.
-
-When a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,
-the system creates a *delayed assignment*. This consists of
-1. A metavariable `?m` of type `(x : α) → (y : β) → γ x y` whose local context is the local context outside the `fun`,
-  where `γ x y` is the type of `?s`. Recall that `x` and `y` appear in the local context of `?s`.
-2. A delayed assignment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`
-
-Then, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here
-as being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.
-
-Once `?s` is fully solved for, in the sense that after metavariable instantiation it is a metavariable-free term `e`,
-then we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.
-(Implementation note: Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables, to skip forming this function.)
-This delayed assignment mechanism is essential to the operation of basic tactics like `intro`,
-and a good mental model is that it is a way to "apply" the metavariable `?s` by substituting values in for some of its local variables.
-While it would be easier to immediately assign `?s := ?m x y`,
-delayed assignment preserves `?s` as an unsolved-for metavariable with a local context that still contains `x` and `y`,
-which is exactly what tactics like `intro` need.
-
-By default, delayed assigned metavariables pretty print with what they are delayed assigned to.
-The delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.
-
-For more information, see the "Gruesome details" module docstrings in `Lean.MetavarContext`.
--/
-@[builtin_term_parser] def syntheticHole := leading_parser
-  "?" >> (ident <|> "_")
-/--
-The `⋯` term denotes a term that was omitted by the pretty printer.
-The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
-and these options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.
-
-It is only meant to be used for pretty printing.
-However, in case it is copied and pasted from the Infoview, `⋯` logs a warning and elaborates like `_`.
--/
-@[builtin_term_parser] def omission := leading_parser
-  "⋯"
-def binderIdent : Parser  := ident <|> hole
 /--
 The `sorry` term is a temporary placeholder for a missing proof or value.
 
@@ -287,8 +196,6 @@ are turned into a new anonymous constructor application. For example,
 -/
 @[builtin_term_parser] def anonymousCtor := leading_parser
   "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
-def optIdent : Parser :=
-  optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser
   "from " >> termParser
 def showRhs := fromTerm <|> byTactic'
@@ -299,8 +206,6 @@ an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
 @[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
-def typeSpec := leading_parser " : " >> termParser
-def optType : Parser := optional typeSpec
 /--
 `@x` disables automatic insertion of implicit parameters of the constant `x`.
 `@e` for any term `e` also disables the insertion of implicit lambdas at this position.
@@ -313,77 +218,6 @@ In contrast to regular patterns, `e` may be an arbitrary term of the appropriate
 -/
 @[builtin_term_parser] def inaccessible := leading_parser
   ".(" >> withoutPosition termParser >> ")"
-def binderType (requireType := false) : Parser :=
-  if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := leading_parser
-  atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
-def binderDefault := leading_parser
-  " := " >> termParser
-
-open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
-@[combinator_parenthesizer Lean.Parser.Term.binderDefault, expose] def binderDefault.parenthesizer : Parenthesizer := do
-  let prec := match (← getCur) with
-    -- must parenthesize to distinguish from `binderTactic`
-    | `(binderDefault| := by $_) => maxPrec
-    | _                          => 0
-  visitArgs do
-    term.parenthesizer prec
-    visitToken
-
-/--
-Explicit binder, like `(x y : A)` or `(x y)`.
-Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
--/
-@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
-  "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
-/--
-Implicit binder, like `{x y : A}` or `{x y}`.
-In regular applications, whenever all parameters before it have been specified,
-then a `_` placeholder is automatically inserted for this parameter.
-Implicit parameters should be able to be determined from the other arguments and the return type
-by unification.
-
-In `@` explicit mode, implicit binders behave like explicit binders.
--/
-@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
-  "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
-def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
-def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
-/--
-Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
-In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
-a `_` placeholder until at least one subsequent explicit parameter is specified.
-Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
-Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
-
-Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
-then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
-and `h hs` has type `p y`.
-In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
-with `?m` a fresh metavariable.
--/
-@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
-  strictImplicitLeftBracket >> many1 binderIdent >>
-  binderType requireType >> strictImplicitRightBracket
-/--
-Instance-implicit binder, like `[C]` or `[inst : C]`.
-In regular applications without `@` explicit mode, it is automatically inserted
-and solved for by typeclass inference for the specified class `C`.
-In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
-use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
--/
-@[builtin_doc] def instBinder := leading_parser ppGroup <|
-  "[" >> withoutPosition (optIdent >> termParser) >> "]"
-/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
-* An explicit binder like `(x y : A)`
-* An implicit binder like `{x y : A}`
-* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
-* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
--/
-@[builtin_doc] def bracketedBinder (requireType := false) :=
-  withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
-    explicitBinder requireType <|> strictImplicitBinder requireType <|>
-    implicitBinder requireType <|> instBinder
 
 /-
 It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
@@ -486,34 +320,6 @@ e.g. because it has no constructors.
 
 @[builtin_term_parser] def «nofun» := leading_parser "nofun"
 
-/-
-Syntax category for structure instance notation fields.
-Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible.
--/
-builtin_initialize
-  registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl
-@[inline] def structInstFieldDeclParser (rbp : Nat := 0) : Parser :=
-  categoryParser `structInstFieldDecl rbp
-def optEllipsis := leading_parser
-  optional " .."
-def structInstArrayRef := leading_parser
-  "[" >> withoutPosition termParser >> "]"
-def structInstLVal := leading_parser
-  (ident <|> fieldIdx <|> structInstArrayRef) >>
-  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
-def structInstFieldBinder :=
-  withAntiquot (mkAntiquot "structInstFieldBinder" decl_name% (isPseudoKind := true)) <|
-    binderIdent <|> bracketedBinder
-def optTypeForStructInst : Parser := optional (atomic (typeSpec >> notFollowedBy "}" "}"))
-/- `x` is an abbreviation for `x := x` -/
-def structInstField := ppGroup <| leading_parser
-  structInstLVal >> optional (many (checkColGt >> ppSpace >> structInstFieldBinder) >> optTypeForStructInst >> ppDedent structInstFieldDeclParser)
-/-
-Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
-This node is used to enable structure instance field completion in the whitespace
-of a structure instance notation.
--/
-def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
 /--
 Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
 inherited. If `e` is itself a variable called `x`, it can be elided:

src/Lean/Parser/Term/Basic.lean

@@ -0,0 +1,286 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
+-/
+module
+
+prelude
+public import Lean.Parser.Attr
+public import Lean.Parser.Level
+public import Lean.Parser.Term.Doc
+meta import Lean.Parser.Basic
+
+
+public section
+
+namespace Lean
+namespace Parser
+
+
+builtin_initialize
+  registerBuiltinParserAttribute `builtin_tactic_parser ``Category.tactic .both
+  registerBuiltinDynamicParserAttribute `tactic_parser `tactic
+
+@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
+  categoryParser `tactic rbp
+
+@[inline] def convParser (rbp : Nat := 0) : Parser :=
+  categoryParser `conv rbp
+
+namespace Tactic
+
+/-- `sepByIndentSemicolon(p)` parses a sequence of `p` optionally followed by `;`,
+similar to `manyIndent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
+the `;` is mandatory. This is used by tactic parsing, so that
+```
+example := by
+  skip
+  skip
+```
+is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
+@[run_builtin_parser_attribute_hooks, builtin_doc]
+def sepByIndentSemicolon (p : Parser) : Parser :=
+  sepByIndent p "; " (allowTrailingSep := true)
+
+/-- `sepBy1IndentSemicolon(p)` parses a (nonempty) sequence of `p` optionally followed by `;`,
+similar to `many1Indent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
+the `;` is mandatory. This is used by tactic parsing, so that
+```
+example := by
+  skip
+  skip
+```
+is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
+@[run_builtin_parser_attribute_hooks, builtin_doc]
+def sepBy1IndentSemicolon (p : Parser) : Parser :=
+  sepBy1Indent p "; " (allowTrailingSep := true)
+
+builtin_initialize
+  register_parser_alias sepByIndentSemicolon
+  register_parser_alias sepBy1IndentSemicolon
+
+@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
+  sepBy1IndentSemicolon tacticParser
+/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
+It runs the tactics in sequence, and fails if the goal is not solved. -/
+@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
+  "{ " >> sepByIndentSemicolon tacticParser >> ppDedent ppLine >> "}"
+
+/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
+Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
+@[builtin_doc, run_builtin_parser_attribute_hooks] def tacticSeq := leading_parser
+  tacticSeqBracketed <|> tacticSeq1Indented
+
+/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
+The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
+position set. -/
+@[builtin_doc, run_builtin_parser_attribute_hooks]
+def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
+  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
+
+/- Raw sequence for quotation and grouping -/
+@[run_builtin_parser_attribute_hooks]
+def seq1 :=
+  node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true)
+
+end Tactic
+
+namespace Term
+/--
+A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
+For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.
+
+The way this works is that holes create fresh metavariables.
+The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
+This is often known as *unification*.
+
+Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
+* In `match` patterns, holes are catch-all patterns.
+* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.
+
+Related concept: implicit parameters are automatically filled in with holes during the elaboration process.
+
+See also `?m` syntax (synthetic holes).
+-/
+@[builtin_term_parser] def hole := leading_parser
+  "_"
+/--
+A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should be synthesized using tactics.
+- `?_` creates a fresh metavariable with an auto-generated name.
+- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.
+
+In particular, the synthetic hole syntax creates "synthetic opaque metavariables",
+the same kind of metavariable used to represent goals in the tactic state.
+
+Synthetic holes are similar to holes in that `_` also creates metavariables,
+but synthetic opaque metavariables have some different properties:
+- In tactics such as `refine`, only synthetic holes yield new goals.
+- During elaboration, unification will not solve for synthetic opaque metavariables, they are "opaque".
+  This is to prevent counterintuitive behavior such as disappearing goals.
+- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
+
+## Delayed assigned metavariables
+
+This section gives an overview of some technical details of synthetic holes, which you should feel free to skip.
+Understanding delayed assignments is mainly useful for those who are working on tactics and other metaprogramming.
+It is included here until there is a suitable place for it in the reference manual.
+
+When a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,
+the system creates a *delayed assignment*. This consists of
+1. A metavariable `?m` of type `(x : α) → (y : β) → γ x y` whose local context is the local context outside the `fun`,
+  where `γ x y` is the type of `?s`. Recall that `x` and `y` appear in the local context of `?s`.
+2. A delayed assignment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`
+
+Then, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here
+as being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.
+
+Once `?s` is fully solved for, in the sense that after metavariable instantiation it is a metavariable-free term `e`,
+then we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.
+(Implementation note: Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables, to skip forming this function.)
+This delayed assignment mechanism is essential to the operation of basic tactics like `intro`,
+and a good mental model is that it is a way to "apply" the metavariable `?s` by substituting values in for some of its local variables.
+While it would be easier to immediately assign `?s := ?m x y`,
+delayed assignment preserves `?s` as an unsolved-for metavariable with a local context that still contains `x` and `y`,
+which is exactly what tactics like `intro` need.
+
+By default, delayed assigned metavariables pretty print with what they are delayed assigned to.
+The delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.
+
+For more information, see the "Gruesome details" module docstrings in `Lean.MetavarContext`.
+-/
+@[builtin_term_parser] def syntheticHole := leading_parser
+  "?" >> (ident <|> "_")
+
+/--
+The `⋯` term denotes a term that was omitted by the pretty printer.
+The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
+and these options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.
+
+It is only meant to be used for pretty printing.
+However, in case it is copied and pasted from the Infoview, `⋯` logs a warning and elaborates like `_`.
+-/
+@[builtin_term_parser] def omission := leading_parser
+  "⋯"
+@[run_builtin_parser_attribute_hooks]
+def binderIdent : Parser  := ident <|> hole
+
+@[run_builtin_parser_attribute_hooks]
+def binderType (requireType := false) : Parser :=
+  if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
+@[run_builtin_parser_attribute_hooks]
+def binderTactic  := leading_parser
+  atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
+def binderDefault := leading_parser
+  " := " >> termParser
+
+open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
+@[combinator_parenthesizer Lean.Parser.Term.binderDefault, expose] def binderDefault.parenthesizer : Parenthesizer := do
+  let prec := match (← getCur) with
+    -- must parenthesize to distinguish from `binderTactic`
+    | `(binderDefault| := by $_) => maxPrec
+    | _                          => 0
+  visitArgs do
+    term.parenthesizer prec
+    visitToken
+
+/--
+Explicit binder, like `(x y : A)` or `(x y)`.
+Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
+-/
+@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
+  "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
+/--
+Implicit binder, like `{x y : A}` or `{x y}`.
+In regular applications, whenever all parameters before it have been specified,
+then a `_` placeholder is automatically inserted for this parameter.
+Implicit parameters should be able to be determined from the other arguments and the return type
+by unification.
+
+In `@` explicit mode, implicit binders behave like explicit binders.
+-/
+@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
+  "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
+def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
+def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
+/--
+Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
+In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
+a `_` placeholder until at least one subsequent explicit parameter is specified.
+Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
+Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
+
+Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
+then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
+and `h hs` has type `p y`.
+In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
+with `?m` a fresh metavariable.
+-/
+@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
+  strictImplicitLeftBracket >> many1 binderIdent >>
+  binderType requireType >> strictImplicitRightBracket
+
+def optIdent : Parser :=
+  optional (atomic (ident >> " : "))
+
+/--
+Instance-implicit binder, like `[C]` or `[inst : C]`.
+In regular applications without `@` explicit mode, it is automatically inserted
+and solved for by typeclass inference for the specified class `C`.
+In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
+use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
+-/
+@[builtin_doc] def instBinder := leading_parser ppGroup <|
+  "[" >> withoutPosition (optIdent >> termParser) >> "]"
+/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
+* An explicit binder like `(x y : A)`
+* An implicit binder like `{x y : A}`
+* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
+* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
+-/
+@[builtin_doc, run_builtin_parser_attribute_hooks] def bracketedBinder (requireType := false) :=
+  withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
+    explicitBinder requireType <|> strictImplicitBinder requireType <|>
+    implicitBinder requireType <|> instBinder
+
+@[run_builtin_parser_attribute_hooks]
+def typeSpec := leading_parser " : " >> termParser
+
+@[run_builtin_parser_attribute_hooks]
+def optType : Parser := optional typeSpec
+
+/-
+Syntax category for structure instance notation fields.
+Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible.
+-/
+builtin_initialize
+  registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl
+@[inline] def structInstFieldDeclParser (rbp : Nat := 0) : Parser :=
+  categoryParser `structInstFieldDecl rbp
+@[run_builtin_parser_attribute_hooks]
+def optEllipsis := leading_parser
+  optional " .."
+@[run_builtin_parser_attribute_hooks]
+def structInstArrayRef := leading_parser
+  "[" >> withoutPosition termParser >> "]"
+@[run_builtin_parser_attribute_hooks]
+def structInstLVal := leading_parser
+  (ident <|> fieldIdx <|> structInstArrayRef) >>
+  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
+@[run_builtin_parser_attribute_hooks]
+def structInstFieldBinder :=
+  withAntiquot (mkAntiquot "structInstFieldBinder" decl_name% (isPseudoKind := true)) <|
+    binderIdent <|> bracketedBinder
+@[run_builtin_parser_attribute_hooks]
+def optTypeForStructInst : Parser := optional (atomic (typeSpec >> notFollowedBy "}" "}"))
+/- `x` is an abbreviation for `x := x` -/
+@[run_builtin_parser_attribute_hooks]
+def structInstField := ppGroup <| leading_parser
+  structInstLVal >> optional (many (checkColGt >> ppSpace >> structInstFieldBinder) >> optTypeForStructInst >> ppDedent structInstFieldDeclParser)
+/-
+Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
+This node is used to enable structure instance field completion in the whitespace
+of a structure instance notation.
+-/
+@[run_builtin_parser_attribute_hooks]
+def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Server.Requests
+import Lean.DocString.Syntax
 
 public section
 
@@ -23,9 +24,13 @@ def noHighlightKinds : Array SyntaxNodeKind := #[
   ``Lean.Parser.Term.type,
   ``Lean.Parser.Term.prop,
   -- not really keywords
-  `antiquotName,
+  `antiquotName]
+
+def docKinds : Array SyntaxNodeKind := #[
+  ``Lean.Parser.Command.plainDocComment,
   ``Lean.Parser.Command.docComment,
-  ``Lean.Parser.Command.moduleDoc]
+  ``Lean.Parser.Command.moduleDoc
+]
 
 -- TODO: make extensible, or don't
 /-- Keywords for which a specific semantic token is provided. -/
@@ -93,6 +98,131 @@ def computeDeltaLspSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Se
     lastPos := pos
   return { data }
 
+open Lean.Doc.Syntax in
+def isVersoKind (k : SyntaxNodeKind) : Bool :=
+  (`Lean.Doc.Syntax).isPrefixOf k
+
+
+open Lean.Doc.Syntax in
+private partial def collectVersoTokens
+    (stx : Syntax) (getTokens : (stx : Syntax) → Array LeanSemanticToken) :
+    Array LeanSemanticToken :=
+  go stx |>.run #[] |>.2
+where
+  tok (tk : Syntax) (k : SemanticTokenType) : StateM (Array LeanSemanticToken) Unit :=
+    modify (·.push ⟨tk, k⟩)
+
+  go (stx : Syntax) : StateM (Array LeanSemanticToken) Unit := do
+  match stx with
+  | `(arg_val| $x:ident )
+  | `(arg_val| $x:str )
+  | `(arg_val| $x:num ) =>
+    tok x .parameter
+  | `(named| (%$tk1 $x:ident :=%$tk2 $v:arg_val )%$tk3) =>
+    tok tk1 .keyword
+    tok x .property
+    tok tk2 .keyword
+    go v
+    tok tk3 .keyword
+  | `(named_no_paren| $x:ident :=%$tk $v:arg_val ) =>
+    tok x .property
+    tok tk .keyword
+    go v
+  | `(flag_on| +%$tk$x)  | `(flag_off| -%$tk$x) =>
+    tok tk .keyword
+    tok x .property
+  | `(link_target| [%$tk1 $s ]%$tk2) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+  | `(link_target| (%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+  | `(inline|$_:str) | `(inline|line! $_) => pure () -- No tokens for plain text or line breaks
+  | `(inline| *[%$tk1 $inls* ]%$tk2) | `(inline|_[%$tk1 $inls* ]%$tk2) =>
+    tok tk1 .keyword
+    inls.forM go
+    tok tk2 .keyword
+  | `(inline| link[%$tk1 $inls* ]%$tk2 $ref) =>
+    tok tk1 .keyword
+    inls.forM go
+    tok tk2 .keyword
+    go ref
+  | `(inline| image(%$tk1 $s )%$tk2 $ref) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+    go ref
+  | `(inline| footnote(%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+  | `(inline| code(%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+  | `(inline| role{%$tk1 $x $args* }%$tk2 [%$tk3 $inls* ]%$tk4) =>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok tk2 .keyword
+    tok tk3 .keyword
+    inls.forM go
+    tok tk4 .keyword
+  | `(inline| \math%$tk1 code(%$tk2 $s )%$tk3)
+  | `(inline| \displaymath%$tk1 code(%$tk2 $s )%$tk3) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+    tok tk3 .keyword
+  | `(list_item| *%$tk $inls*) =>
+    tok tk .keyword
+    inls.forM go
+  | `(desc| :%$tk $inls* => $blks*) =>
+    tok tk .keyword
+    inls.forM go
+    blks.forM go
+  | `(block|para[$inl*]) => inl.forM go
+  | `(block| ```%$tk1 $x $args* | $s ```%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok s .string
+    tok tk2 .keyword
+  | `(block| :::%$tk1 $x $args* { $blks* }%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    blks.forM go
+    tok tk2 .keyword
+  | `(block| command{%$tk1 $x $args*}%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok tk2 .keyword
+  | `(block| %%%%$tk1 $vals* %%%%$tk2)=>
+    tok tk1 .keyword
+    modify (· ++ getTokens (mkNullNode vals))
+    tok tk2 .keyword
+  | `(block| [%$tk1 $s ]:%$tk2 $url) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+    tok url .string
+  | `(block| [^%$tk1 $s ]:%$tk2 $inls*) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+    inls.forM go
+  | `(block| header(%$tk $_ ){ $inls* })=>
+    tok tk .keyword
+    inls.forM go
+  | `(block|ul{$items*}) | `(block|ol($_){$items*}) | `(block|dl{$items*}) =>
+    items.forM go
+  | _ =>
+    pure ()
+
 /--
 Collects all semantic tokens that can be deduced purely from `Syntax`
 without elaboration information.
@@ -107,6 +237,12 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
   | stx => Id.run do
     if noHighlightKinds.contains stx.getKind then
       return #[]
+    if docKinds.contains stx.getKind then
+      -- Docs are only highlighted in Verso format, in which case `stx[1]` is a node.
+      if stx[1].isAtom then
+        return #[]
+      else
+        return collectVersoTokens stx[1] collectSyntaxBasedSemanticTokens
     let mut tokens :=
       if stx.isOfKind choiceKind then
         collectSyntaxBasedSemanticTokens stx[0]
@@ -120,10 +256,12 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
       return tokens
     return tokens.push ⟨stx, keywordSemanticTokenMap.getD val .keyword⟩
 
+
+open Lean.Doc.Syntax in
 /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/
 def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken :=
-  List.toArray <| i.deepestNodes fun _ i _ => do
-    let .ofTermInfo ti := i
+  Array.flatten <| List.toArray <| i.deepestNodes fun _ info _ => do
+    let .ofTermInfo ti := info
       | none
     let .original .. := ti.stx.getHeadInfo
       | none
@@ -133,11 +271,11 @@ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken
           -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition.
           if localDecl.isAuxDecl then
             if ti.isBinder then
-              return ⟨ti.stx, SemanticTokenType.function⟩
+              return #[⟨ti.stx, SemanticTokenType.function⟩]
           else if ! localDecl.isImplementationDetail then
-            return ⟨ti.stx, SemanticTokenType.variable⟩
+            return #[⟨ti.stx, SemanticTokenType.variable⟩]
     if ti.stx.getKind == Parser.Term.identProjKind then
-      return ⟨ti.stx, SemanticTokenType.property⟩
+      return #[⟨ti.stx, SemanticTokenType.property⟩]
     none
 
 def computeSemanticTokens  (doc : EditableDocument) (beginPos : String.Pos)

src/Lean/Server/GoTo.lean

@@ -324,6 +324,8 @@ def locationLinksOfInfo (doc : DocumentMeta) (kind : GoToKind) (ictx : InfoWithC
         locationLinksFromCommandInfo cci
       | .ofErrorNameInfo eni =>
         locationLinksFromErrorNameInfo eni
+      | .ofDocElabInfo dei =>
+        locationLinksFromDecl dei.name
       | _ =>
         pure #[]
     if kind == .declaration || ll.isEmpty then

src/Lean/Server/InfoUtils.lean

@@ -186,6 +186,8 @@ def Info.stx : Info → Syntax
   | ofFieldRedeclInfo i    => i.stx
   | ofDelabTermInfo i      => i.stx
   | ofChoiceInfo i         => i.stx
+  | ofDocInfo i            => i.stx
+  | ofDocElabInfo i        => i.stx
 
 def Info.lctx : Info → LocalContext
   | .ofTermInfo i           => i.lctx
@@ -343,6 +345,10 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   | .ofErrorNameInfo eni => do
     let some errorExplanation := getErrorExplanationRaw? (← getEnv) eni.errorName | return none
     return errorExplanation.summaryWithSeverity
+  | .ofDocInfo di =>
+    return (← findDocString? env di.stx.getKind)
+  | .ofDocElabInfo dei =>
+    return (← findDocString? env dei.name)
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator

src/Lean/Server/References.lean

@@ -252,6 +252,8 @@ def identOf (ci : ContextInfo) (i : Info) : Option (RefIdent × Bool) := do
     some (RefIdent.const (← getModuleContainingDecl? ci.env fi.projName).toString fi.projName.toString, false)
   | Info.ofOptionInfo oi =>
     some (RefIdent.const (← getModuleContainingDecl? ci.env oi.declName).toString oi.declName.toString, false)
+  | Info.ofDocElabInfo dei =>
+    some (RefIdent.const (← getModuleContainingDecl? ci.env dei.name).toString dei.name.toString, false)
   | _ => none
 
 /-- Finds all references in `trees`. -/

src/Std/Do/Triple/SpecLemmas.lean

@@ -340,8 +340,8 @@ A loop invariant is a `PostCond` that takes as parameters
   `let mut` variables and early return.
 
 The loop specification lemmas will use this in the following way:
-Before entering the loop, the zipper's prefix is empty and the suffix is `xs`.
-After leaving the loop, the zipper's suffix is empty and the prefix is `xs`.
+Before entering the loop, the cursor's prefix is empty and the suffix is `xs`.
+After leaving the loop, the cursor's prefix is `xs` and the suffix is empty.
 During the induction step, the invariant holds for a suffix with head element `x`.
 After running the loop body, the invariant then holds after shifting `x` to the prefix.
 -/

src/Std/Internal/Async/Basic.lean

@@ -369,10 +369,10 @@ def joinTask (t : Task (MaybeTask α)) : Task α :=
     | .pure a => .pure a
     | .ofTask t => t
 
-instance : Functor (MaybeTask) where
+instance : Functor MaybeTask where
   map := MaybeTask.map
 
-instance : Monad (MaybeTask) where
+instance : Monad MaybeTask where
   pure := MaybeTask.pure
   bind := MaybeTask.bind
 
@@ -494,6 +494,69 @@ instance : MonadAsync Task BaseAsync where
 instance [Inhabited α] : Inhabited (BaseAsync α) where
   default := .mk <| pure (MaybeTask.pure default)
 
+instance : MonadFinally BaseAsync where
+  tryFinally' x f := do
+    let res ← x
+    Prod.mk res <$> f (some res)
+
+/--
+Converts `Except` to `BaseAsync`.
+-/
+@[inline]
+protected def ofExcept (except : Except Empty α) : BaseAsync α :=
+  pure (f := BaseIO) <| MaybeTask.pure <| match except with | .ok res => res
+
+/--
+Runs two computations concurrently and returns both results as a pair.
+-/
+@[inline, specialize]
+def concurrently (x : BaseAsync α) (y : BaseAsync β) (prio := Task.Priority.default) : BaseAsync (α × β) := do
+  let taskX : Task _ ← MonadAsync.async x (prio := prio)
+  let taskY : Task _ ← MonadAsync.async y (prio := prio)
+  let resultX ← MonadAwait.await taskX
+  let resultY ← MonadAwait.await taskY
+  return (resultX, resultY)
+
+/--
+Runs two computations concurrently and returns the result of the one that finishes first.
+The other result is lost and the other task is not cancelled, so the task will continue the execution
+until the end.
+-/
+@[inline, specialize]
+def race [Inhabited α] (x : BaseAsync α) (y : BaseAsync α) (prio := Task.Priority.default) : BaseAsync α := do
+  let promise ← IO.Promise.new
+
+  let task₁ : Task _ ← MonadAsync.async (prio := prio) x
+  let task₂ : Task _ ← MonadAsync.async (prio := prio) y
+
+  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
+
+  MonadAwait.await promise.result!
+
+/--
+Runs all computations in an `Array` concurrently and returns all results as an array.
+-/
+@[inline, specialize]
+def concurrentlyAll (xs : Array (BaseAsync α)) (prio := Task.Priority.default) :  BaseAsync (Array α) := do
+  let tasks : Array (Task α) ← xs.mapM (MonadAsync.async (prio := prio))
+  tasks.mapM MonadAwait.await
+
+/--
+Runs all computations concurrently and returns the result of the first one to finish.
+All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+until the end.
+-/
+@[inline, specialize]
+def raceAll [Inhabited α] [ForM BaseAsync c (BaseAsync α)] (xs : c) (prio := Task.Priority.default) : BaseAsync α := do
+  let promise ← IO.Promise.new
+
+  ForM.forM xs fun x => do
+    let task₁ ← MonadAsync.async (t := Task) (prio := prio) x
+    BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+
+  MonadAwait.await promise.result!
+
 end BaseAsync
 
 /--
@@ -578,6 +641,13 @@ Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.
 protected def asTask (x : EAsync ε α) (prio := Task.Priority.default) : EIO ε (ETask ε α) :=
   x |> BaseAsync.asTask (prio := prio)
 
+/--
+Block until the `EAsync` finishes and returns its value. Propagates any error encountered during execution.
+-/
+@[inline]
+protected def block (x : EAsync ε α) (prio := Task.Priority.default) : EIO ε α :=
+  x.asTask (prio := prio) >>= ETask.block
+
 /--
 Raises an error of type `ε` within the `EAsync` monad.
 -/
@@ -707,6 +777,68 @@ protected partial def forIn
 instance : ForIn (EAsync ε) Lean.Loop Unit where
   forIn _ := EAsync.forIn
 
+/--
+Converts `Except` to `EAsync`.
+-/
+@[inline]
+protected def ofExcept (except : Except ε α) : EAsync ε α :=
+  pure (f := BaseIO) (MaybeTask.pure except)
+
+/--
+Runs two computations concurrently and returns both results as a pair.
+-/
+@[inline, specialize]
+def concurrently (x : EAsync ε α) (y : EAsync ε β) (prio := Task.Priority.default) : EAsync ε (α × β) := do
+  let taskX : ETask ε _ ← MonadAsync.async x (prio := prio)
+  let taskY : ETask ε _ ← MonadAsync.async y (prio := prio)
+  let resultX ← MonadAwait.await taskX
+  let resultY ← MonadAwait.await taskY
+  return (resultX, resultY)
+
+/--
+Runs two computations concurrently and returns the result of the one that finishes first.
+The other result is lost and the other task is not cancelled, so the task will continue the execution
+until the end.
+-/
+@[inline, specialize]
+def race [Inhabited α] (x : EAsync ε α) (y : EAsync ε α)
+    (prio := Task.Priority.default) :
+    EAsync ε α := do
+  let promise ← IO.Promise.new
+
+  let task₁ : ETask ε _ ← MonadAsync.async (prio := prio) x
+  let task₂ : ETask ε _ ← MonadAsync.async (prio := prio) y
+
+  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
+
+  let result ← MonadAwait.await promise.result!
+  EAsync.ofExcept result
+
+/--
+Runs all computations in an `Array` concurrently and returns all results as an array.
+-/
+@[inline, specialize]
+def concurrentlyAll (xs : Array (EAsync ε α)) (prio := Task.Priority.default) : EAsync ε (Array α) := do
+  let tasks : Array (ETask ε α) ← xs.mapM (MonadAsync.async (prio := prio))
+  tasks.mapM MonadAwait.await
+
+/--
+Runs all computations concurrently and returns the result of the first one to finish.
+All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+until the end.
+-/
+@[inline, specialize]
+def raceAll [Inhabited α] [ForM (EAsync ε) c (EAsync ε α)] (xs : c) (prio := Task.Priority.default) : EAsync ε α := do
+  let promise ← IO.Promise.new
+
+  ForM.forM xs fun x => do
+    let task₁ ← MonadAsync.async (t := ETask ε) (prio := prio) x
+    BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+
+  let result ← MonadAwait.await promise.result!
+  EAsync.ofExcept result
+
 end EAsync
 
 /--
@@ -723,6 +855,61 @@ Converts a `Async` to a `AsyncTask`.
 protected def toIO (x : Async α) : IO (AsyncTask α) :=
   MaybeTask.toTask <$> x.toRawBaseIO
 
+/--
+Block until the `Async` finishes and returns its value. Propagates any error encountered during execution.
+-/
+@[inline]
+protected def block (x : Async α) (prio := Task.Priority.default) : IO α :=
+  x.asTask (prio := prio) >>= ETask.block
+
+/--
+Converts `Promise` into `Async`.
+-/
+@[inline]
+protected def ofPromise (task : IO (IO.Promise (Except IO.Error α))) : Async α := do
+  match ← task.toBaseIO with
+  | .ok data => pure (f := BaseIO) (MaybeTask.ofTask data.result!)
+  | .error err => pure (f := BaseIO) (MaybeTask.pure (.error err))
+
+/--
+Converts `AsyncTask` into `Async`.
+-/
+@[inline]
+protected def ofAsyncTask (task : AsyncTask α) : Async α := do
+  pure (f := BaseIO) (MaybeTask.ofTask task)
+
+/--
+Converts `IO (Task α)` into `Async`.
+-/
+@[inline]
+protected def ofIOTask (task : IO (Task α)) : Async α := do
+  match ← task.toBaseIO with
+  | .ok data => .ofAsyncTask (data.map Except.ok)
+  | .error err => pure (f := BaseIO) (MaybeTask.pure (.error err))
+
+/--
+Converts `Except` to `Async`.
+-/
+@[inline]
+protected def ofExcept (except : Except IO.Error α) : Async α :=
+  pure (f := BaseIO) (MaybeTask.pure except)
+
+/--
+Converts `Task` to `Async`.
+-/
+@[inline]
+protected def ofTask (task : Task α) : Async α := do
+  .ofAsyncTask (task.map Except.ok)
+
+/--
+Converts `IO (IO.Promise α)` to `Async`.
+-/
+@[inline]
+protected def ofPurePromise (task : IO (IO.Promise α)) : Async α := do
+  match ← task.toBaseIO with
+  | .ok data => pure (f := BaseIO) (MaybeTask.ofTask <| data.result!.map (.ok))
+  | .error err => pure (f := BaseIO) (MaybeTask.pure (.error err))
+
 @[default_instance]
 instance : MonadAsync AsyncTask Async :=
   inferInstanceAs (MonadAsync (ETask IO.Error) (EAsync IO.Error))
@@ -733,6 +920,61 @@ instance : MonadAwait AsyncTask Async :=
 instance : MonadAwait IO.Promise Async :=
   inferInstanceAs (MonadAwait IO.Promise (EAsync IO.Error))
 
+/--
+Runs two computations concurrently and returns both results as a pair.
+-/
+@[inline, specialize]
+def concurrently (x : Async α) (y : Async β) (prio := Task.Priority.default) : Async (α × β) := do
+  let taskX ← MonadAsync.async x (prio := prio)
+  let taskY ← MonadAsync.async y (prio := prio)
+  let resultX ← MonadAwait.await taskX
+  let resultY ← MonadAwait.await taskY
+  return (resultX, resultY)
+
+/--
+Runs two computations concurrently and returns the result of the one that finishes first.
+The other result is lost and the other task is not cancelled, so the task will continue the execution
+until the end.
+-/
+@[inline, specialize]
+def race [Inhabited α] (x : Async α) (y : Async α)
+    (prio := Task.Priority.default) :
+    Async α := do
+  let promise ← IO.Promise.new
+
+  let task₁ ← MonadAsync.async (t := AsyncTask) (prio := prio) x
+  let task₂ ← MonadAsync.async (t := AsyncTask) (prio := prio) y
+
+  BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+  BaseIO.chainTask task₂ (liftM ∘ promise.resolve)
+
+  let result ← MonadAwait.await promise.result!
+  Async.ofExcept result
+
+/--
+Runs all computations in an `Array` concurrently and returns all results as an array.
+-/
+@[inline, specialize]
+def concurrentlyAll (xs : Array (Async α)) (prio := Task.Priority.default) : Async (Array α) := do
+  let tasks : Array (AsyncTask α) ← xs.mapM (MonadAsync.async (prio := prio))
+  tasks.mapM MonadAwait.await
+
+/--
+Runs all computations concurrently and returns the result of the first one to finish.
+All other results are lost, and the tasks are not cancelled, so they'll continue their executing
+until the end.
+-/
+@[inline, specialize]
+def raceAll [ForM Async c (Async α)] (xs : c) (prio := Task.Priority.default) : Async α := do
+  let promise ← IO.Promise.new
+
+  ForM.forM xs fun x => do
+    let task₁ ← MonadAsync.async (t := AsyncTask) (prio := prio) x
+    BaseIO.chainTask task₁ (liftM ∘ promise.resolve)
+
+  let result ← MonadAwait.await promise.result!
+  Async.ofExcept result
+
 end Async
 
 export MonadAsync (async)
@@ -745,69 +987,6 @@ This function transforms the operation inside the monad `m` into a task and let
 def background [Monad m] [MonadAsync t m] (action : m α) (prio := Task.Priority.default) : m Unit :=
   discard (async (t := t) (prio := prio) action)
 
-/--
-Runs two computations concurrently and returns both results as a pair.
--/
-@[inline, specialize]
-def concurrently
-    [Monad m] [MonadAwait t m] [MonadAsync t m]
-    (x : m α) (y : m β)
-    (prio := Task.Priority.default) :
-    m (α × β) := do
-  let taskX : t α ← async x (prio := prio)
-  let taskY : t β ← async y (prio := prio)
-  let resultX ← await taskX
-  let resultY ← await taskY
-  return (resultX, resultY)
-
-/--
-Runs two computations concurrently and returns the result of the one that finishes first.
-The other result is lost and the other task is not cancelled, so the task will continue the execution
-until the end.
--/
-@[inline, specialize]
-def race
-    [MonadLiftT BaseIO m] [MonadAwait Task m] [MonadAsync t m] [MonadAwait t m]
-    [Monad m] [Inhabited α] (x : m α) (y : m α)
-    (prio := Task.Priority.default) :
-    m α := do
-  let promise ← IO.Promise.new
-
-  discard (async (t := t) (prio := prio) <| Bind.bind x (liftM ∘ promise.resolve))
-  discard (async (t := t) (prio := prio) <| Bind.bind y (liftM ∘ promise.resolve))
-
-  await promise.result!
-
-/--
-Runs all computations in an `Array` concurrently and returns all results as an array.
--/
-@[inline, specialize]
-def concurrentlyAll
-    [Monad m] [MonadAwait t m] [MonadAsync t m] (xs : Array (m α))
-    (prio := Task.Priority.default) :
-    m (Array α) := do
-  let tasks : Array (t α) ← xs.mapM (async (prio := prio))
-  tasks.mapM await
-
-/--
-Runs all computations concurrently and returns the result of the first one to finish.
-All other results are lost, and the tasks are not cancelled, so they'll continue their executing
-until the end.
--/
-@[inline, specialize]
-def raceAll
-    [ForM m c (m α)] [MonadLiftT BaseIO m] [MonadAwait Task m]
-    [MonadAsync t m] [MonadAwait t m] [Monad m] [Inhabited α]
-    (xs : c)
-    (prio := Task.Priority.default) :
-    m α := do
-  let promise ← IO.Promise.new
-
-  ForM.forM xs fun x =>
-    discard (async (t := t) (prio := prio) <| Bind.bind x (liftM ∘ promise.resolve))
-
-  await promise.result!
-
 end Async
 end IO
 end Internal

src/Std/Internal/Async/DNS.lean

@@ -39,10 +39,11 @@ structure NameInfo where
 Asynchronously resolves a hostname and service to an array of socket addresses.
 -/
 @[inline]
-def getAddrInfo (host : String) (service : String) (addressFamily : Option AddressFamily := none) :
-    IO (AsyncTask (Array IPAddr)) :=
-  AsyncTask.ofPromise <$> UV.DNS.getAddrInfo host service
-    (match addressFamily with
+def getAddrInfo (host : String) (service : String) (addrFamily : Option AddressFamily := none) : Async (Array IPAddr) := do
+  Async.ofPromise <| UV.DNS.getAddrInfo
+    host
+    service
+    (match addrFamily with
     | none => 0
     | some .ipv4 => 1
     | some .ipv6 => 2)
@@ -51,9 +52,10 @@ def getAddrInfo (host : String) (service : String) (addressFamily : Option Addre
 Performs a reverse DNS lookup on a `SocketAddress`.
 -/
 @[inline]
-def getNameInfo (host : @& SocketAddress) : IO (AsyncTask NameInfo) :=
+def getNameInfo (host : @& SocketAddress) : Async NameInfo :=
   UV.DNS.getNameInfo host
-  |>.map (Task.map (.map <| Function.uncurry NameInfo.mk) ∘ AsyncTask.ofPromise)
+  |> Async.ofPromise
+  |>.map (Function.uncurry NameInfo.mk)
 
 end DNS
 end Async

src/Std/Internal/Async/Select.lean

@@ -72,18 +72,18 @@ structure Selector (α : Type) where
   Attempts to retrieve a piece of data from the event source in a non-blocking fashion, returning
   `some` if data is available and `none` otherwise.
   -/
-  tryFn : IO (Option α)
+  tryFn : Async (Option α)
   /--
   Registers a `Waiter` with the event source. Once data is available, the event source should
   attempt to call `Waiter.race` and resolve the `Waiter`'s promise if it wins. It is crucial that
   data is never actually consumed from the event source unless `Waiter.race` wins in order to
   prevent data loss.
   -/
-  registerFn : Waiter α → IO Unit
+  registerFn : Waiter α → Async Unit
   /--
   A cleanup function that is called once any `Selector` has won the `Selectable.one` race.
   -/
-  unregisterFn : IO Unit
+  unregisterFn : Async Unit
 
 /--
 An event source together with a continuation to call on data obtained from that event source,
@@ -99,7 +99,7 @@ structure Selectable (α : Type) where
     /--
     The continuation that is called on results from the event source.
     -/
-    cont : β → IO (AsyncTask α)
+    cont : β → Async α
 
 private def shuffleIt {α : Type u} (xs : Array α) (gen : StdGen) : Array α :=
   go xs gen 0
@@ -123,16 +123,18 @@ The protocol for this is as follows:
    Once one of them resolves the `Waiter`, all `Selector.unregisterFn` functions are called, and
    the `Selectable.cont` of the winning `Selector` is executed and returned.
 -/
-partial def Selectable.one (selectables : Array (Selectable α)) : IO (AsyncTask α) := do
+partial def Selectable.one (selectables : Array (Selectable α)) : Async α := do
   if selectables.isEmpty then
     throw <| .userError "Selectable.one requires at least one Selectable"
 
   let seed := UInt64.toNat (ByteArray.toUInt64LE! (← IO.getRandomBytes 8))
   let gen := mkStdGen seed
   let selectables := shuffleIt selectables gen
+
   for selectable in selectables do
     if let some val ← selectable.selector.tryFn then
-      return ← selectable.cont val
+      let result ← selectable.cont val
+      return result
 
   let finished ← IO.mkRef false
   let promise ← IO.Promise.new
@@ -142,27 +144,30 @@ partial def Selectable.one (selectables : Array (Selectable α)) : IO (AsyncTask
     let waiter := Waiter.mk finished waiterPromise
     selectable.selector.registerFn waiter
 
-    IO.chainTask (t := waiterPromise.result?) fun res? => do
+    discard <| IO.bindTask (t := waiterPromise.result?) fun res? => do
       match res? with
       | none =>
         /-
         If we get `none` that means the waiterPromise was dropped, usually due to cancellation. In
         this situation just do nothing.
         -/
-        return ()
+        return (Task.pure (.ok ()))
       | some res =>
-        try
-          let res ← IO.ofExcept res
+        let async : Async _ :=
+          try
+            let res ← IO.ofExcept res
 
-          for selectable in selectables do
-            selectable.selector.unregisterFn
+            for selectable in selectables do
+              selectable.selector.unregisterFn
 
-          let contRes ← selectable.cont res
-          discard <| contRes.mapIO (promise.resolve <| .ok ·)
-        catch e =>
-          promise.resolve (.error e)
+            let contRes ← selectable.cont res
+            promise.resolve (.ok contRes)
+          catch e =>
+            promise.resolve (.error e)
 
-  return AsyncTask.ofPromise promise
+        async.toBaseIO
+
+  Async.ofPromise (pure promise)
 
 end Async
 end IO

src/Std/Internal/Async/TCP.lean

@@ -18,7 +18,6 @@ namespace Internal
 namespace IO
 namespace Async
 namespace TCP
-
 open Std.Net
 
 namespace Socket
@@ -66,9 +65,10 @@ def listen (s : Server) (backlog : UInt32) : IO Unit :=
 Accepts an incoming connection.
 -/
 @[inline]
-def accept (s : Server) : IO (AsyncTask Client) := do
-  let conn ← s.native.accept
-  return conn.result!.map (·.map Client.ofNative)
+def accept (s : Server) : Async Client := do
+  s.native.accept
+  |> Async.ofPromise
+  |>.map Client.ofNative
 
 /--
 Gets the local address of the server socket.
@@ -115,15 +115,15 @@ def bind (s : Client) (addr : SocketAddress) : IO Unit :=
 Connects the client socket to the given address.
 -/
 @[inline]
-def connect (s : Client) (addr : SocketAddress) : IO (AsyncTask Unit) :=
-  AsyncTask.ofPromise <$> s.native.connect addr
+def connect (s : Client) (addr : SocketAddress) : Async Unit :=
+  Async.ofPromise <| s.native.connect addr
 
 /--
 Sends data through the client socket.
 -/
 @[inline]
-def send (s : Client) (data : ByteArray) : IO (AsyncTask Unit) :=
-  AsyncTask.ofPromise <$> s.native.send data
+def send (s : Client) (data : ByteArray) : Async Unit :=
+  Async.ofPromise <| s.native.send data
 
 /--
 Receives data from the client socket. If data is received, it’s wrapped in .some. If EOF is reached,
@@ -132,21 +132,21 @@ socket is not supported. Instead, we recommend binding multiple sockets to the s
 Furthermore calling this function in parallel with `recvSelector` is not supported.
 -/
 @[inline]
-def recv? (s : Client) (size : UInt64) : IO (AsyncTask (Option ByteArray)) :=
-  AsyncTask.ofPromise <$> s.native.recv? size
+def recv? (s : Client) (size : UInt64) : Async (Option ByteArray) :=
+  Async.ofPromise <| s.native.recv? size
 
 /--
 Creates a `Selector` that resolves once `s` has data available, up to at most `size` bytes,
 and provides that data. Calling this function starts the data wait, so it must not be called
 in parallel with `recv?`.
 -/
-def recvSelector (s : TCP.Socket.Client) (size : UInt64) : IO (Selector (Option ByteArray)) := do
+def recvSelector (s : TCP.Socket.Client) (size : UInt64) : Async (Selector (Option ByteArray)) := do
   let readableWaiter ← s.native.waitReadable
   return {
     tryFn := do
       if ← readableWaiter.isResolved then
         -- We know that this read should not block
-        let res ← (← s.recv? size).block
+        let res ← (s.recv? size).block
         return some res
       else
         return none
@@ -161,7 +161,7 @@ def recvSelector (s : TCP.Socket.Client) (size : UInt64) : IO (Selector (Option
             try
               discard <| IO.ofExcept res
               -- We know that this read should not block
-              let res ← (← s.recv? size).block
+              let res ← (s.recv? size).block
               promise.resolve (.ok res)
             catch e =>
               promise.resolve (.error e)
@@ -173,8 +173,8 @@ def recvSelector (s : TCP.Socket.Client) (size : UInt64) : IO (Selector (Option
 Shuts down the write side of the client socket.
 -/
 @[inline]
-def shutdown (s : Client) : IO (AsyncTask Unit) :=
-  AsyncTask.ofPromise <$> s.native.shutdown
+def shutdown (s : Client) : Async Unit :=
+  Async.ofPromise <| s.native.shutdown
 
 /--
 Gets the remote address of the client socket.
@@ -205,7 +205,6 @@ def keepAlive (s : Client) (enable : Bool) (delay : Std.Time.Second.Offset) (_ :
   s.native.keepAlive enable.toInt8 delay.val.toNat.toUInt32
 
 end Client
-
 end Socket
 end TCP
 end Async