Examples.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 26 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned Theorem Proving in Lean documentation, Pinned Theorem Proving in Lean 4 book index

98 declarations, 7 contain sorry, 0 declared as axioms

Imports (5)

SubVerso.Examples
Lean.Data.NameMap
Lean.DocString.Syntax
VersoManual
Verso.Code.HighlightedToTex

def TPiL.projectDir line 20 source
def TPiL.alphabet line 22 source
no axioms what this means
Statement uses: String
def TPiL.hashString line 24 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: UInt64, String
Proof uses: Id.run, Nat, UInt64.toNat, Bind.bind, Id, Prod, ForIn.forIn, Lean.Loop, Unit, Lean.Loop.mk, Prod.mk, Prod.fst, Prod.snd, ite, ForInStep, GT.gt, OfNat.ofNat, String.push, String.Pos.Raw.get!, TPiL.alphabet and 6 more
12 instances, coercions and auxiliary constants left out.
def TPiL.exampleSubversoRev The SubVerso revision recorded in the example project's Lake manifest line 45 source
Source documentation
The SubVerso revision recorded in the example project's Lake manifest.
That revision writes the extracted JSON, and the copy of SubVerso that Verso brings in here reads it back, so the serialization the two agree on is part of what an extraction depends on.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadError, MonadLiftT, BaseIO, IO, String
Proof uses: System.FilePath, HDiv.hDiv, System.FilePath.mk, Bind.bind, Bool, liftM, System.FilePath.pathExists, Unit, EIO, IO.Error, IO.FS.readFile, TPiL.exampleSubversoRev.match_4, Except, Lean.Json, Lean.Json.parse, TPiL.exampleSubversoRev.match_3, Array, Lean.Json.getObjValAs?, Prod, Option and 22 more
19 instances, coercions and auxiliary constants left out.
```
def exampleSubversoRev : m String := do
…
```
Mentions: m
def TPiL.extractFile Extracts the highlighted contents of an example line 69 source
Source documentation
Extracts the highlighted contents of an example.
When expectErrors is set, building the example is allowed to fail: the errors it reports are described in the document, and checked against the extracted messages there. Extraction itself must still succeed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Monad, Lean.MonadError, MonadLiftT, BaseIO, IO, MonadFinally, Lean.MonadTrace, Lean.AddMessageContext, Lean.MonadOptions, Lean.MonadAlwaysExcept, String, Option, optParam, Bool, Bool.false, Array, SubVerso.Module.ModuleItem
Proof uses: System.FilePath, HDiv.hDiv, System.FilePath.mk, Bind.bind, liftM, System.FilePath.pathExists, Unit, EIO, IO.Error, IO.FS.readFile, Pure.pure, String.Slice.copy, String.trimAscii, TPiL.exampleSubversoRev, UInt64, Hashable.hash, Prod, Prod.mk, TPiL.hashString, HAppend.hAppend and 57 more
27 instances, coercions and auxiliary constants left out.
```
def extractFile (contents : String) (suppressNamespaces : Option String)
    (expectErrors : Bool := false) : m (Array ModuleItem) := do
…
```
Mentions: m
def TPiL.hasAtLeastM line 180 source
def TPiL.hasAtLeast line 190 source
def TPiL.splitExample line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Prod, Option
Proof uses: Id.run, Array, SubVerso.Highlighting.Highlighted.lines, SubVerso.Highlighting.Highlighted.empty, Bind.bind, Id, ForIn'.forIn', Std.Legacy.Range, Nat, inferInstance, Membership, Std.Legacy.Range.mk, OfNat.ofNat, Array.size, Nat.zero_lt_one, Prod.mk, Option.none, Membership.mem, Prod.fst, Prod.snd and 18 more
15 instances, coercions and auxiliary constants left out.
def TPiL.hlIsWs line 207 source
no axioms what this means
Statement uses: SubVerso.Highlighting.Highlighted, Bool
Proof uses: Inhabited.default
1 instances, coercions and auxiliary constants left out.
inductive TPiL.LineType line 220 source
def TPiL.lineType line 225 source
def TPiL.detachPrefix line 232 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Array, SubVerso.Module.ModuleItem, Prod, Option
Proof uses: Id.run, List.toArray, List.nil, Bind.bind, Id, ForIn'.forIn', Std.Legacy.Range, Nat, inferInstance, Membership, Std.Legacy.Range.mk, OfNat.ofNat, Array.size, Nat.zero_lt_one, Prod.mk, Option.none, Membership.mem, Prod.fst, Prod.snd, SubVerso.Highlighting.Highlighted and 30 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def TPiL.detachSuffix line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Array, SubVerso.Module.ModuleItem, Prod, Option
Proof uses: Id.run, List.toArray, List.nil, Bind.bind, Id, ForIn'.forIn', Std.Legacy.Range, Nat, inferInstance, Membership, Std.Legacy.Range.mk, OfNat.ofNat, Array.size, Nat.zero_lt_one, Prod.mk, Option.none, Membership.mem, Prod.fst, Prod.snd, HSub.hSub and 30 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def TPiL.splitExample' line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Array, SubVerso.Module.ModuleItem, Prod, Option
Proof uses: TPiL.splitExample'.match_2, TPiL.detachPrefix, TPiL.splitExample'.match_1, TPiL.detachSuffix, Prod.mk
def TPiL.copyButtonCss line 306 source
no axioms what this means
Statement uses: String
def TPiL.copyButtonJs line 375 source
no axioms what this means
Statement uses: String
def TPiL.examplesCss line 547 source
no axioms what this means
Statement uses: String
def TPiL.tpilBlock line 559 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Genre.Manual.BlockDescr
Proof uses: Verso.Genre.Manual.BlockDescr.mk, Verso.Genre.Manual.HtmlAssets.mk, Verso.Genre.Manual.HtmlAssets.features, Verso.Genre.Manual.BlockDescr.toHtmlAssets, Verso.Genre.Manual.HtmlAssets.extraCss, Verso.Genre.Manual.HtmlAssets.extraJs, Std.HashSet.insert, Verso.Genre.Manual.JsFile, Verso.Genre.Manual.HtmlAssets.extraJsFiles, Verso.Genre.Manual.JsFile.mk, Verso.Genre.Manual.StaticJsFile.mk, Bool.false, List.toArray, String, List.nil, Verso.Genre.Manual.JS.mk, TPiL.copyButtonJs, Option.none, Verso.Genre.Manual.JsSourceMap, Verso.Genre.Manual.CssFile and 15 more
4 instances, coercions and auxiliary constants left out.
def TPiL.tpilInline line 571 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Genre.Manual.InlineDescr
Proof uses: Verso.Genre.Manual.InlineDescr.mk, Verso.Genre.Manual.HtmlAssets.mk, Verso.Genre.Manual.HtmlAssets.features, Verso.Genre.Manual.InlineDescr.toHtmlAssets, Verso.Genre.Manual.HtmlAssets.extraCss, Verso.Genre.Manual.HtmlAssets.extraJs, Std.HashSet.insert, Verso.Genre.Manual.JsFile, Verso.Genre.Manual.HtmlAssets.extraJsFiles, Verso.Genre.Manual.JsFile.mk, Verso.Genre.Manual.StaticJsFile.mk, Bool.false, List.toArray, String, List.nil, Verso.Genre.Manual.JS.mk, TPiL.copyButtonJs, Option.none, Verso.Genre.Manual.JsSourceMap, Verso.Genre.Manual.CssFile and 15 more
4 instances, coercions and auxiliary constants left out.
structure TPiL.ExampleItem line 582 source
no axioms what this means
def TPiL.verbatimBlock line 588 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Verso.Output.TeX
Proof uses: SubVerso.Highlighting.Highlighted.toVerbatimTeX, SubVerso.Highlighting.Highlighted.trimOneLeadingNl, SubVerso.Highlighting.Highlighted.trimOneTrailingNl, Bool.false, Verso.Output.TeX.seq, List.toArray, List.cons, Verso.Output.TeX.raw, ToString.toString, String, List.nil
1 instances, coercions and auxiliary constants left out.
def TPiL.proofStateStyle line 814 source
no axioms what this means
Statement uses: String
def TPiL.kbdCSS line 919 source
no axioms what this means
Statement uses: String
def TPiL.oneCodeStr line 993 source
def TPiL.codeStrs line 1000 source
structure TPiL.Kept line 1013 source
no axioms what this means

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
instance TPiL.(instance at line 1019) line 1019 source
def TPiL.Kept.add line 1022 source
standard axioms: Quot.sound, propext what this means
Statement uses: TPiL.Kept
Proof uses: TPiL.Kept.mk, Array.set, TPiL.Kept.values, TPiL.Kept.next, TPiL.Kept.in_bounds, ite, Nat, Eq, OfNat.ofNat, HSub.hSub, Array.size
5 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance TPiL.(instance at line 1030) line 1030 source
instance TPiL.(instance at line 1039) line 1039 source
def TPiL.allProofInfo line 1052 source
standard axioms: Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Array
Proof uses: TPiL.allProofInfo.go, List.toArray, List.nil
def TPiL.saveBackref line 1069 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Verso.Doc.Elab.DocElabM, Unit
Proof uses: Array.foldl, HAppend.hAppend, SubVerso.Highlighting.Highlighted.text, TPiL.allProofInfo, OfNat.ofNat, Nat, Array.size, Lean.MonadEnv.modifyEnv, Lean.Environment, Lean.EnvExtension.modifyState, TPiL.Kept, TPiL.recentHighlightsExt, TPiL.Kept.add, Lean.EnvExtension.asyncMode, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.
structure TPiL.ProofState line 1076 source
no axioms what this means
def TPiL.allInfo Extracts all messages from the given code line 1087 source
Source documentation
Extracts all messages from the given code.

standard axioms: Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Array, Prod, SubVerso.Highlighting.Highlighted.Message, Option
Proof uses: WellFounded.fix, WellFoundedRelation, invImage, TPiL.allInfo.match_2, SubVerso.Highlighting.Highlighted.seq, Array.flatMap, Subtype, Membership.mem, Array.map_unattach.match_1, Array.attach, SubVerso.Highlighting.Highlighted.Span.Kind, SubVerso.Highlighting.Highlighted.MessageContents, SubVerso.Highlighting.Highlighted.point, List.toArray, List.cons, Prod.mk, SubVerso.Highlighting.Highlighted.Message.mk, Option.none, List.nil, SubVerso.Highlighting.Highlighted.Goal and 12 more
9 instances, coercions and auxiliary constants left out.
```
def allInfo (hl : Highlighted) : Array (Highlighted.Message × Option Highlighted) :=
…
```
def TPiL.trailingText Splits the trailing text off some code line 1101 source
Source documentation
Splits the trailing text off some code.
Comments are read as text only when comments is set. Everywhere else they are part of the code and are shown as they were written.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, optParam, Bool, Bool.false, Prod, String
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def trailingText (hl : Highlighted) (comments := false) : Highlighted × String :=
…
```
def TPiL.messageComment? Splits the marker that introduces a message off a comment's text, along with the severity it names, if any line 1132 source
Source documentation
Splits the marker that introduces a message off a comment's text, along with the severity it names, if any.
A comment below a command describes the message it produces only when marked this way, which tells it apart from a comment that remarks on the code.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, Option, Prod
Proof uses: String.Slice, String.trimAsciiStart, ite, Eq, Bool, Bool.not, String.Slice.startsWith, Bool.true, Option.none, String.Slice.drop, String.length, Option.some, Prod.mk, String.Slice.copy, String.Slice.trimAsciiStart, OfNat.ofNat, Nat, TPiL.messageComment?.match_2, List, Std.Iter.toList and 17 more
16 instances, coercions and auxiliary constants left out.
```
def messageComment? (s : String) : Option (Option String × String) :=
…
```
structure TPiL.ExpectedMessage A comment that describes the message a command produces line 1155 source
Source documentation
A comment that describes the message a command produces.

no axioms what this means
```
structure ExpectedMessage where
…
```
def TPiL.commentContents Extracts the text of a comment, which may span several lines line 1169 source
Source documentation
Extracts the text of a comment, which may span several lines.
Each line contributes its content after the delimiter and the single space that conventionally follows it. Any further indentation is part of the text, because messages indent their details.
```
private def commentContents (s : String) : Option ExpectedMessage :=
…
```
Mentions: TPiL.ExpectedMessage
def TPiL.expectedComment The comment that describes a message line 1190 source
Source documentation
The comment that describes a message.
A message of one line is written on the command's own line; a longer one is written on the lines below it, at the command's indentation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String
Proof uses: HAppend.hAppend, List, List.map, String.Slice, String.Slice.copy, Std.Iter.toList, Std.Iterators.Types.Map, String.Slice.SplitIterator, String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher, Char, Bool, BEq.beq, Char.ofNat, String.toSlice, String.Slice.Subslice, Id, MonadLiftT.monadLift, Pure.pure, Std.Iterators.PostconditionT, String.Slice.Subslice.toSlice and 10 more
16 instances, coercions and auxiliary constants left out.
```
def expectedComment (indent severity : String) (msg : String) : String :=
…
```
def TPiL.messageSeverityName The name of a message's severity line 1203 source
Source documentation
The name of a message's severity.

no axioms what this means
Statement uses: SubVerso.Highlighting.Highlighted.Message, String
Proof uses: TPiL.messageSeverityName.match_1, SubVerso.Highlighting.Highlighted.Span.Kind, SubVerso.Highlighting.Highlighted.Message.severity, Unit
```
def messageSeverityName (msg : Highlighted.Message) : String :=
…
```
def TPiL.lastLineIndent The indentation of the last line of some code line 1210 source
Source documentation
The indentation of the last line of some code.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String
Proof uses: TPiL.lastLineIndent.match_1, Option, String.Slice, List.getLast?, Std.Iter.toList, Std.Iterators.Types.Map, String.Slice.SplitIterator, String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher, Char, Bool, BEq.beq, Char.ofNat, String.toSlice, String.Slice.Subslice, Id, MonadLiftT.monadLift, Pure.pure, Std.Iterators.PostconditionT, String.Slice.Subslice.toSlice, String.split and 3 more
13 instances, coercions and auxiliary constants left out.
```
def lastLineIndent (s : String) : String :=
…
```
def TPiL.trailingComment Extracts a trailing comment from code, if present line 1220 source
Source documentation
Extracts a trailing comment from code, if present.
Returns the code along with the comment and its trailing whitespace.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Prod, Option, TPiL.ExpectedMessage
Proof uses: String, TPiL.trailingText, Bool.true, TPiL.trailingComment.match_1, Prod.snd, Prod.mk, Prod.fst, Option.some, Unit, Option.none
1 instances, coercions and auxiliary constants left out.
```
def trailingComment (hl : Highlighted) : Highlighted × Option ExpectedMessage :=
…
```
Mentions: TPiL.ExpectedMessage
inductive TPiL.ShowProofStates line 1229 source
no axioms what this means
structure TPiL.LeanConfig line 1234 source
no axioms what this means
instance TPiL.(instance at line 1248) line 1248 source
instance TPiL.(instance at line 1266) line 1266 source
structure TPiL.SavedLeanConfig line 1276 source
no axioms what this means
instance TPiL.(instance at line 1280) line 1280 source
def TPiL.isNewline line 1288 source
standard axioms: Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Bool
Proof uses: WellFounded.fix, WellFoundedRelation, invImage, TPiL.isNewline.match_1, String, SubVerso.Highlighting.Highlighted.text, BEq.beq, SubVerso.Highlighting.Highlighted.unparsed, SubVerso.Highlighting.Token, SubVerso.Highlighting.Highlighted.token, Bool.false, Array, SubVerso.Highlighting.Highlighted.seq, Id.run, Bind.bind, Id, Prod, Option, Unit, ForIn'.forIn' and 35 more
21 instances, coercions and auxiliary constants left out.
def TPiL.commentColumn The column at which the comment on a line begins, if it has one line 1304 source
Source documentation
The column at which the comment on a line begins, if it has one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Option, Nat
Proof uses: Prod.snd, TPiL.commentColumn.go, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
def commentColumn (hl : Highlighted) : Option Nat := (go 0 hl).2
…
```
def TPiL.isMessageCommentLine Whether a line is a comment that introduces a message line 1318 source
Source documentation
Whether a line is a comment that introduces a message.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Bool
Proof uses: String.Slice, String.trimAsciiStart, SubVerso.Highlighting.Highlighted.toString, Bool.and, String.Slice.startsWith, String, Option.isSome, Prod, Option, TPiL.messageComment?, String.Slice.copy, String.Slice.dropWhile, Char, BEq.beq, Char.ofNat
4 instances, coercions and auxiliary constants left out.
```
def isMessageCommentLine (hl : Highlighted) : Bool :=
…
```
def TPiL.isCommentLine Whether a line consists of a comment, along with any surrounding whitespace line 1323 source
Source documentation
Whether a line consists of a comment, along with any surrounding whitespace.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SubVerso.Highlighting.Highlighted, Bool
Proof uses: Bool.and, TPiL.isCommentLine.hasComment, Bool.not, TPiL.isCommentLine.hasCode
```
def isCommentLine (hl : Highlighted) : Bool :=
…
```
def TPiL.fixupAnchorComments Leading anchor comments are always incorrect line 1348 source
Source documentation
Leading anchor comments are always incorrect. They probably result from Lean placing them with the next command, so we should move them back up before processing them.
Line comments form one comment when they share a column, and a comment that describes a command follows it directly: on the command's own line, on the lines below it, or both. Those move back as well. A comment at some other column, or one held off by a blank line, is a separate comment that belongs to the command below it.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Array, SubVerso.Module.ModuleItem
Proof uses: Id.run, List.toArray, List.nil, Option, Option.none, Bind.bind, Id, Prod, ForIn.forIn, inferInstance, Membership, Prod.mk, Prod.fst, Prod.snd, Unit, ForInStep, Option.some, Pure.pure, ForInStep.yield, ite and 48 more
17 instances, coercions and auxiliary constants left out.
```
def fixupAnchorComments (items : Array ModuleItem) : Array ModuleItem := Id.run do
…
```
def TPiL.logCommentMismatch Reports a comment that doesn't describe the message its command produced line 1400 source
Source documentation
Reports a comment that doesn't describe the message its command produced.
The corrected block is offered when the command occurs just once, so that replacing it is unambiguous. Any existing comment is dropped, which moves it to the place that suits the message.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.Syntax.StrLit, String, Lean.MessageData, Verso.Doc.Elab.DocElabM, Unit
Proof uses: List, String.Slice, Std.Iter.toList, Std.Iterators.Types.Map, String.Slice.SplitIterator, String.Slice.Pattern.ForwardSliceSearcher, String.toSlice, Lean.TSyntax.getString, String.Slice.Subslice, Id, MonadLiftT.monadLift, Pure.pure, Std.Iterators.PostconditionT, String.Slice.Subslice.toSlice, String.split, ite, Eq, Bool, BEq.beq, Nat and 59 more
36 instances, coercions and auxiliary constants left out.
```
def logCommentMismatch (block : StrLit) (itemText strippedText severity msg : String)
    (what : MessageData) : DocElabM Unit := do
…
```
def TPiL.checkSeverity Reports a comment that names a severity other than the one its command produced line 1423 source
Source documentation
Reports a comment that names a severity other than the one its command produced.
A comment that names no severity describes a message of any kind.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.Syntax.StrLit, String, TPiL.ExpectedMessage, SubVerso.Highlighting.Highlighted.Message, Verso.Doc.Elab.DocElabM, Unit
Proof uses: TPiL.messageSeverityName, TPiL.extractFile.match_1, Option, TPiL.ExpectedMessage.severity, ite, Eq, Bool, BEq.beq, Bool.true, Pure.pure, Unit.unit, TPiL.logCommentMismatch, SubVerso.Highlighting.Highlighted.Message.toString, List.nil, Lean.Name, HAppend.hAppend, Lean.MessageData, Lean.ToMessageData.toMessageData
9 instances, coercions and auxiliary constants left out.
```
def checkSeverity (block : StrLit) (itemText strippedText : String)
    (expected : ExpectedMessage) (msg : Highlighted.Message) : DocElabM Unit := do
…
```
Mentions: TPiL.ExpectedMessage
def TPiL.showGoals line 1431 source
def TPiL.lean line 1444 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, TPiL.LeanConfig, Verso.ArgParse.parseThe, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 158 more
56 instances, coercions and auxiliary constants left out.
def TPiL.save line 1547 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, TPiL.SavedLeanConfig, Verso.ArgParse.parseThe, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 66 more
42 instances, coercions and auxiliary constants left out.
def TPiL.savedAnchor line 1569 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, Lean.Syntax.Ident, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 65 more
43 instances, coercions and auxiliary constants left out.
structure TPiL.ProofStateConfig line 1581 source
no axioms what this means
structure TPiL.GoalConfig line 1584 source
no axioms what this means
def TPiL.strOrName line 1589 source
instance TPiL.(instance at line 1597) line 1597 source
instance TPiL.(instance at line 1600) line 1600 source
def TPiL.proofState sorry line 1606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, TPiL.ProofStateConfig, Verso.ArgParse.parseThe, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 95 more
44 instances, coercions and auxiliary constants left out.
def TPiL.goal sorry line 1626 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, TPiL.GoalConfig, Verso.ArgParse.parseThe, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 89 more
40 instances, coercions and auxiliary constants left out.
structure TPiL.Helper line 1647 source
no axioms what this means
def TPiL.Helper.fromModule line 1655 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, IO, TPiL.Helper
Proof uses: UInt64, Hashable.hash, HAppend.hAppend, TPiL.hashString, System.FilePath, HDiv.hDiv, System.FilePath.mk, Bind.bind, IO.Error, Bool, liftM, BaseIO, EIO, System.FilePath.pathExists, Unit, IO.FS.readFile, Pure.pure, String.Slice.copy, String.trimAscii, IO.FS.writeFile and 79 more
34 instances, coercions and auxiliary constants left out.
def TPiL.setup line 1801 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.DirectiveExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.setup.match_1, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 50 more
32 instances, coercions and auxiliary constants left out.
def TPiL.prioritizedElab line 1821 source
standard axioms: Quot.sound, propext what this means
Statement uses: Monad, Bool, Array
Proof uses: Prod, Nat, List.toArray, List.nil, Bind.bind, ForIn'.forIn', Std.Legacy.Range, inferInstance, Membership, Std.Legacy.Range.mk, OfNat.ofNat, Array.size, Nat.zero_lt_one, Prod.mk, Membership.mem, Prod.fst, Prod.snd, GetElem.getElem, LT.lt, ForInStep and 12 more
16 instances, coercions and auxiliary constants left out.
def TPiL.isLeanBlock line 1835 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, Lean.Core.CoreM, Bool
Proof uses: ite, Eq, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Lean.Name.mkStr4, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Lean.Syntax.matchesNull, cond, Bool.or, Bool.false, Lean.TSyntax.mk, Lean.TSyntaxArray, Lean.TSyntaxArray.mk, Lean.Syntax.getArgs, Bind.bind, Lean.Name and 12 more
9 instances, coercions and auxiliary constants left out.
def TPiL.leanFirst Elaborates Lean blocks first, maintaining the order of blocks line 1846 source
Source documentation
Elaborates Lean blocks first, maintaining the order of blocks. This makes their code available for leanRef.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.DirectiveExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.setup.match_1, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 16 more
19 instances, coercions and auxiliary constants left out.
```
def leanFirst : DirectiveExpander
  | args, contents => do
    ArgParse.done.run args

    -- Elaborate Lean blocks first, so inlines in prior blocks can refer to them
    prioritizedElab (isLeanBlock ·) elabBlock contents


@[code_block_expander setup]
```
Mentions: in, TPiL.prioritizedElab, TPiL.isLeanBlock, TPiL.setup
def TPiL.setupCode line 1855 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 19 more
23 instances, coercions and auxiliary constants left out.
def TPiL.comment line 1863 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.DirectiveExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.setup.match_1, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Pure.pure, List.toArray
3 instances, coercions and auxiliary constants left out.
def TPiL.TODO line 1867 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.DirectiveExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.setup.match_1, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Pure.pure, List.toArray
3 instances, coercions and auxiliary constants left out.
def TPiL.TODOinline line 1871 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Pure.pure, List.toArray
3 instances, coercions and auxiliary constants left out.
def TPiL.kw line 1875 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 45 more
32 instances, coercions and auxiliary constants left out.
def TPiL.attr line 1883 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 45 more
32 instances, coercions and auxiliary constants left out.
def TPiL.tactic line 1892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 45 more
32 instances, coercions and auxiliary constants left out.
def TPiL.kbd line 1900 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 39 more
32 instances, coercions and auxiliary constants left out.
def TPiL.option line 1907 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 30 more
31 instances, coercions and auxiliary constants left out.
def TPiL.currentHelper line 1914 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.DocElabM, TPiL.Helper
Proof uses: Bind.bind, Lean.Environment, Lean.MonadEnv.getEnv, TPiL.currentHelper.match_1, Option, Lean.EnvExtension.getState, TPiL.helperExt, Lean.EnvExtension.asyncMode, Lean.Name.anonymous, Pure.pure, TPiL.defaultHelperExt, Lean.Name, Lean.getMainModule, liftM, EIO, IO.Error, IO, TPiL.Helper.fromModule, HAppend.hAppend, String and 5 more
14 instances, coercions and auxiliary constants left out.
def TPiL.multiVar? line 1922 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, Option, Prod, Array
Proof uses: List.toArray, List.nil, String.Slice, String.trimAscii, Bind.bind, ForIn.forIn, Lean.Loop, Unit, Lean.Loop.mk, Prod.mk, Option.none, Prod.snd, Prod.fst, String.Slice.takeWhile, Char, Bool, TPiL.multiVar?.alpha, Nat, Std.Iter.length, String.Slice.PosIterator and 36 more
19 instances, coercions and auxiliary constants left out.
def TPiL.highlightInline line 1949 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, optParam, Option, Option.none, Verso.Doc.Elab.DocElabM, SubVerso.Highlighting.Highlighted
Proof uses: Bind.bind, TPiL.Helper, TPiL.currentHelper, MonadExcept.tryCatch, Lean.Exception, Unit, TPiL.highlightInline.match_1, Prod, Array, TPiL.multiVar?, SubVerso.Highlighting.Highlighted.empty, ForIn.forIn, inferInstance, Membership, ForInStep, liftM, EIO, IO.Error, IO, TPiL.Helper.highlight and 23 more
26 instances, coercions and auxiliary constants left out.
def TPiL.highlightCommand line 1969 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, Verso.Doc.Elab.DocElabM, SubVerso.Highlighting.Highlighted
Proof uses: Bind.bind, TPiL.Helper, TPiL.currentHelper, liftM, EIO, IO.Error, IO, TPiL.Helper.command
5 instances, coercions and auxiliary constants left out.
def TPiL.highlightSignature line 1973 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, Verso.Doc.Elab.DocElabM, SubVerso.Highlighting.Highlighted
Proof uses: Bind.bind, TPiL.Helper, TPiL.currentHelper, liftM, EIO, IO.Error, IO, TPiL.Helper.signature
5 instances, coercions and auxiliary constants left out.
def TPiL.highlightName line 1977 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: String, Verso.Doc.Elab.DocElabM, SubVerso.Highlighting.Highlighted
Proof uses: Bind.bind, TPiL.Helper, TPiL.currentHelper, liftM, EIO, IO.Error, IO, TPiL.Helper.name
5 instances, coercions and auxiliary constants left out.
def TPiL.leanInline sorry line 1982 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, ite, Eq, Bool, Bool.true, Option, String, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM and 63 more
36 instances, coercions and auxiliary constants left out.
def TPiL.name sorry line 2001 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, ite, Eq, Bool, Bool.true, Option, String, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM and 77 more
39 instances, coercions and auxiliary constants left out.
def TPiL.leanCommand sorry line 2039 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 78 more
43 instances, coercions and auxiliary constants left out.
def TPiL.leanCommandBlock sorry line 2062 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 74 more
35 instances, coercions and auxiliary constants left out.
def TPiL.signature sorry line 2084 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.CodeBlockExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.lean.match_13, Verso.Doc.Elab.DocElabM, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context, Lean.Meta.State and 74 more
35 instances, coercions and auxiliary constants left out.
def TPiL.leanRef line 2106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, ite, Eq, Bool, Bool.true, Option, String, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM and 72 more
41 instances, coercions and auxiliary constants left out.
def TPiL.empty line 2124 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Verso.Doc.Elab.RoleExpander
Proof uses: Array, Verso.Doc.Arg, Lean.TSyntaxArray, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr1, List.nil, TPiL.goal.match_4, Verso.Doc.Elab.DocElabM, Lean.TSyntax, Bind.bind, Unit, Verso.ArgParse.run, Lean.Core.CoreM, Lean.Elab.Term.TermElabM, StateRefT', IO.RealWorld, Lean.Elab.Term.State, Lean.Meta.MetaM, Lean.Elab.Term.Context and 8 more
22 instances, coercions and auxiliary constants left out.
def TPiL.keywords line 2129 source
def TPiL.tactics line 2138 source
def TPiL.leanLits line 2144 source
def TPiL.suggest Internal detail of suggestion mechanism line 2154 source
Source documentation
Internal detail of suggestion mechanism.
```
private def suggest : InlineExpander
  |  `(inline| code( $str )) => do
    let str' := str.getString
…
```