Documentation
Lean.Meta.Structure
Google site search
Lean.Meta.Structure
source
Imports
Init
Lean.Structure
Lean.Meta.AppBuilder
Imported by
Lean.Meta.getStructureName
source
def
Lean.Meta.getStructureName
(struct :
Lean.Expr
)
:
Lean.MetaM
Lean.Name
Equations
One or more equations did not get rendered due to their size.