Documentation
Lean
.
Elab
.
RecommendedSpelling
Search
return to top
source
Imports
Lean.Elab.Command
Lean.Parser.Command
Lean.Parser.Term.Doc
Imported by
Lean
.
Elab
.
Term
.
Doc
.
elabRecommendedSpelling
Lean
.
Elab
.
Term
.
Doc
.
allRecommendedSpellings
source
def
Lean
.
Elab
.
Term
.
Doc
.
elabRecommendedSpelling
:
Command.CommandElab
Equations
Instances For
source
def
Lean
.
Elab
.
Term
.
Doc
.
allRecommendedSpellings
:
MetaM
(
Array
Parser.Term.Doc.RecommendedSpelling
)
Returns an array containing all recommended spellings.
Equations
Instances For