def Lean.Meta.getStructureName (struct : Lean.Expr) : Lean.MetaM Lean.Name

Equations

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