Documentation

Lean.Meta.MethodSpecs

source
structure Lean.MethodSpecsAttrData :
Type
  • clsName : Name
  • privateSpecs : Bool

    Whether the specs should be public or private

Instances For
    source
    instance Lean.instInhabitedMethodSpecsAttrData :
    Inhabited MethodSpecsAttrData
    Equations
      source
      def Lean.instInhabitedMethodSpecsAttrData.default :
      MethodSpecsAttrData
      Equations
        Instances For
          source
          def Lean.getMethodSpecTheorem (instName : Name) (op : String) :
          MetaM (Option Name)
          Equations
            Instances For
              source
              def Lean.getMethodSpecTheorems (instName : Name) (op : String) :
              MetaM (Option (Array Name))
              Equations
                Instances For