@[specialize #[]]

partial def DocGen4.Output.splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos.Raw) (r : List String) : List String

Auxiliary function for splitAround.

def DocGen4.Output.splitAround (s : String) (p : Char → Bool) : List String

Similar to String.split in Lean core, but keeps the separater. e.g. splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]

Equations

• DocGen4.Output.splitAround s p = DocGen4.Output.splitAroundAux s p 0 0 []

def DocGen4.Output.nameToLink? (s : String) : HtmlM (Option String)

Resolve a docstring identifier reference (`Foo.bar or a .lean file path) to a URL.

Resolution order:

1. If the input looks like a source file path (*.lean with a /), construct the corresponding source HTML page URL.
2. Otherwise try to decode it as a Lean.Name. If decoding succeeds: a. Local decl match — present in name2ModIdx and non-private: emit a relative decl link. Auto-generated eliminators (Foo.rec, Foo.casesOn, …) prefer their parent type when the parent is also available. b. Local module match — present in moduleNames: emit a relative module link. c. Similar local decl — fuzzy-match by trailing components against the current module. d. External fallback — emit externalDeclLink name, i.e. the Mathlib find/?pattern=…#doc redirect. Both branches that previously returned none now route here, so cross-references to dep / Lean-core decls in docstrings become clickable.
3. If the input was not a decodable name and not a .lean path, return none (the caller can treat it as plain text).

See docs/dev/design/external-linking.md for the external-link policy.

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.Output.nameToLink?.sameEnd (n1 n2 : Lean.Name) : Bool

Equations

• DocGen4.Output.nameToLink?.sameEnd n1 n2 = (n1.componentsRev.zip n2.componentsRev).all fun (x : Lean.Name × Lean.Name) => match x with | (a, b) => a == b

def DocGen4.Output.extendLink (s : String) : HtmlM String

Extend links with following rules:

1. if the link starts with ##, a name search is used, and will use find if not found
2. if the link starts with #, it's treated as id link, no modification
3. if the link starts with http, it's an absolute one, no modification
4. otherwise it's a relative link, extend it with base url

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.Output.findBibitem? (href : String) (thePrefix : String := "") : HtmlM (Option BibItem)

Find a bibitem if href starts with thePrefix.

Equations

• DocGen4.Output.findBibitem? href thePrefix = if href.startsWith thePrefix = true then do let __do_lift ← read pure __do_lift.refsMap[(href.drop thePrefix.length).copy]? else pure none

def DocGen4.Output.attrTextToString (ts : Array MD4Lean.AttrText) : String

Flattens an array of MD4Lean.AttrText to a plain String.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def DocGen4.Output.textToPlaintext (t : MD4Lean.Text) : String

Extracts plain text from a single MD4Lean.Text, ignoring all formatting.

Equations

• DocGen4.Output.textToPlaintext (MD4Lean.Text.normal s) = s
• DocGen4.Output.textToPlaintext MD4Lean.Text.nullchar = "�"
• DocGen4.Output.textToPlaintext (MD4Lean.Text.br a) = "\n"
• DocGen4.Output.textToPlaintext (MD4Lean.Text.softbr a) = "\n"
• DocGen4.Output.textToPlaintext (MD4Lean.Text.entity s) = s
• DocGen4.Output.textToPlaintext (MD4Lean.Text.em ts) = DocGen4.Output.textsToPlaintext ts
• DocGen4.Output.textToPlaintext (MD4Lean.Text.strong ts) = DocGen4.Output.textsToPlaintext ts
• DocGen4.Output.textToPlaintext (MD4Lean.Text.u ts) = DocGen4.Output.textsToPlaintext ts
• DocGen4.Output.textToPlaintext (MD4Lean.Text.del ts) = DocGen4.Output.textsToPlaintext ts
• DocGen4.Output.textToPlaintext (MD4Lean.Text.a href title isAuto ts) = DocGen4.Output.textsToPlaintext ts
• DocGen4.Output.textToPlaintext (MD4Lean.Text.img src title alt) = DocGen4.Output.textsToPlaintext alt
• DocGen4.Output.textToPlaintext (MD4Lean.Text.code ss) = String.join ss.toList
• DocGen4.Output.textToPlaintext (MD4Lean.Text.latexMath ss) = String.join ss.toList
• DocGen4.Output.textToPlaintext (MD4Lean.Text.latexMathDisplay ss) = String.join ss.toList
• DocGen4.Output.textToPlaintext (MD4Lean.Text.wikiLink target ts) = DocGen4.Output.textsToPlaintext ts

@[irreducible]

def DocGen4.Output.textsToPlaintext (ts : Array MD4Lean.Text) : String

Extract plain text from an array of MD4Lean.Text.

Equations

• DocGen4.Output.textsToPlaintext ts = Array.foldl (fun (str : String) (t : MD4Lean.Text) => str ++ DocGen4.Output.textToPlaintext t) "" ts

def DocGen4.Output.mdGetHeadingId (texts : Array MD4Lean.Text) : String

Generates an id attribute for heading elements, with the following rules:

1. Characters in letter, mark, number and symbol Unicode categories are preserved.
2. Any sequences of characters in punctuation, separator and other categories are replaced by a single dash.
3. Cases (upper and lower) are preserved.

Equations

• DocGen4.Output.mdGetHeadingId texts = DocGen4.Output.mdGetHeadingId.replaceCharSeq DocGen4.Output.mdGetHeadingId.unicodeToDrop "-" (DocGen4.Output.mdGetHeadingId.textsToPlaintext texts)

def DocGen4.Output.mdGetHeadingId.textsToPlaintext (ts : Array MD4Lean.Text) : String

Equations

• DocGen4.Output.mdGetHeadingId.textsToPlaintext ts = String.join (List.map DocGen4.Output.textToPlaintext ts.toList)

def DocGen4.Output.mdGetHeadingId.replaceCharSeq (pattern : Char → Bool) (replacement s : String) : String

Equations

• DocGen4.Output.mdGetHeadingId.replaceCharSeq pattern replacement s = replacement.intercalate (List.filter (fun (x : String) => !x.isEmpty) (s.splitToList pattern))

def DocGen4.Output.mdGetHeadingId.unicodeToDrop (c : Char) : Bool

Equations

• DocGen4.Output.mdGetHeadingId.unicodeToDrop c = decide (c ∈ Unicode.GC.P ||| Unicode.GC.Z ||| Unicode.GC.C)

def DocGen4.Output.isLeanCode (lang : Array MD4Lean.AttrText) : Bool

Checks whether a fenced code block language allows auto-linking.

Equations

• DocGen4.Output.isLeanCode lang = ((DocGen4.Output.attrTextToString lang).isEmpty || DocGen4.Output.attrTextToString lang == "lean")

def DocGen4.Output.autoLinkInline (ss : Array String) : HtmlM (Array Html)

Automatically adds intra-documentation links for code content.

Equations

• One or more equations did not get rendered due to their size.

def DocGen4.Output.autoLinkInline.unicodeToSplit (c : Char) : Bool

Equations

• DocGen4.Output.autoLinkInline.unicodeToSplit c = decide (c ∈ Unicode.GC.Z ||| Unicode.GC.C)

partial def DocGen4.Output.renderText (t : MD4Lean.Text) (funName : String) (inLink : Bool := false) : HtmlM (Array Html)

Renders a single MD4Lean.Text inline element to HTML, while processing custom extensions such as bibliography items. inLink suppresses auto-linking inside <a> to avoid nested anchors.

partial def DocGen4.Output.renderTexts (texts : Array MD4Lean.Text) (funName : String) (inLink : Bool := false) : HtmlM (Array Html)

Render an array of MD4Lean.Text inline elements to HTML.

partial def DocGen4.Output.renderBlock (block : MD4Lean.Block) (funName : String) (tight : Bool := false) : HtmlM (Array Html)

Render a single MD4Lean.Block element to HTML.

partial def DocGen4.Output.renderLi (li : MD4Lean.Li MD4Lean.Block) (funName : String) (tight : Bool) : HtmlM (Array Html)

Render a list item to HTML.

partial def DocGen4.Output.findAllReferences (refsMap : Std.HashMap String BibItem) (s : String) (i : s.Pos := s.startPos) (ret : Std.HashSet String := ∅) : Std.HashSet String

Find all references in a markdown text.

def DocGen4.Output.docStringToHtml (docString : String ⊕ Lean.VersoDocString) (funName : String) : HtmlM (Array Html)

Convert docstring to Html.

Equations

• One or more equations did not get rendered due to their size.