Documentation

Lean.Meta.Tactic.Simp.Attr

def Lean.Meta.mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) (ref : Name := by exact decl_name%) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Meta.registerSimpAttr (attrName : Name) (attrDescr : String) (ref : Name := by exact decl_name%) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.