Environment extension to register preferred spellings of notations in identifiers.

structure Lean.Parser.Term.Doc.RecommendedSpelling : Type

Information about how to spell a certain notation for an identifier in declaration names.

• notation : String

  The notation in question.

• recommendedSpelling : String

  The recommended spelling of the notation in identifiers.

• additionalInformation? : Option String

  Additional information.

opaque Lean.Parser.Term.Doc.recommendedSpellingByNameExt : PersistentEnvExtension (Name × Array RecommendedSpelling) (RecommendedSpelling × Array Name) (NameMap (Array RecommendedSpelling))

Recommended spellings for notations, stored in a way so that the recommended spellings for a given declaration are easily accessible.

opaque Lean.Parser.Term.Doc.recommendedSpellingExt : PersistentEnvExtension RecommendedSpelling RecommendedSpelling (Array RecommendedSpelling)

Recommended spellings for notations, stored in such a way that it is easy to generate a table containing every recommended spelling exactly once.

def Lean.Parser.Term.Doc.addRecommendedSpelling (env : Environment) (rec : RecommendedSpelling) (names : Array Name) : Environment

Adds a recommended spelling to the environment.

def Lean.Parser.Term.Doc.getRecommendedSpellingsForName (env : Environment) (declName : Name) : Array RecommendedSpelling

Returns the recommended spellings associated with the given declaration name.

def Lean.Parser.Term.Doc.getRecommendedSpellingString (env : Environment) (declName : Name) : String

Renders the recommended spellings for the given declaration into a string for appending to the docstring.

def Lean.Parser.Term.Doc.getRecommendedSpellingString.indentLine (str : String) : String

def Lean.Parser.Term.Doc.getRecommendedSpellingString.bullet (spelling : RecommendedSpelling) : String