structure Lean.MethodSpecsAttrData : Type

• clsName : Name
• privateSpecs : Bool

  Whether the specs should be public or private

instance Lean.instInhabitedMethodSpecsAttrData : Inhabited MethodSpecsAttrData

Equations

• Lean.instInhabitedMethodSpecsAttrData = { default := Lean.instInhabitedMethodSpecsAttrData.default }

def Lean.instInhabitedMethodSpecsAttrData.default : MethodSpecsAttrData

Equations

• Lean.instInhabitedMethodSpecsAttrData.default = { clsName := default, privateSpecs := default }

def Lean.getMethodSpecTheorem (instName : Name) (op : String) : MetaM (Option Name)

Equations

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

def Lean.getMethodSpecTheorems (instName : Name) (op : String) : MetaM (Option (Array Name))

Equations

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