def DocGen4.Process.getTacticExtensionText (env : Lean.Environment) (tactic : Lean.Name) : Option (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)

Gets the rendered extensions for the given canonical tactic name as Verso content

Equations

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

def DocGen4.Process.getRecommendedSpellingText (env : Lean.Environment) (declName : Lean.Name) : Option (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)

Renders the recommended spellings for the given declaration into Verso content for appending to the docstring.

Equations

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

def DocGen4.Process.getRecommendedSpellingText.bullet (spelling : Lean.Parser.Term.Doc.RecommendedSpelling) : Lean.Doc.ListItem (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)

Equations

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

def DocGen4.Process.getDocString? (env : Lean.Environment) (name : Lean.Name) : IO (Option (String ⊕ Lean.VersoDocString))

Equations

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

def DocGen4.Process.NameInfo.ofTypedName (n : Lean.Name) (t : Lean.Expr) : Lean.MetaM NameInfo

Equations

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

def DocGen4.Process.Info.ofTypedName (n : Lean.Name) (t : Lean.Expr) : Lean.MetaM Info

Equations

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

def DocGen4.Process.Info.ofConstantVal (v : Lean.ConstantVal) : Lean.MetaM Info

Equations

• DocGen4.Process.Info.ofConstantVal v = do let __do_lift ← Lean.Meta.inferType (Lean.Expr.const v.name (List.map Lean.mkLevelParam v.levelParams)) DocGen4.Process.Info.ofTypedName v.name __do_lift