def Lean.Doc.Parser.versoSyntaxToString (stx : Syntax) (alternate : Bool := false) : String

Equations

• Lean.Doc.Parser.versoSyntaxToString stx alternate = Lean.Doc.Parser.oneTrailingNewline✝ (Lean.Doc.Parser.separatedToString✝ stx alternate)

def Lean.Doc.Parser.versoDocumentToString (blocks : TSyntaxArray `Lean.Doc.Parser.block) : String

Renders a sequence of blocks as Verso.

Equations

• Lean.Doc.Parser.versoDocumentToString blocks = Lean.Doc.Parser.oneTrailingNewline✝ (Vector.foldl (fun (x1 x2 : String) => x1 ++ x2) "" (Lean.Doc.Parser.versoBlocksToString✝ blocks))

def Lean.Doc.Parser.document.formatter : PrettyPrinter.Formatter

Equations

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