Documentation

Lean.Elab.PreDefinition.Structural.Eqns

source
structure Lean.Elab.Structural.EqnInfo :
Type
Instances For
    source
    def Lean.Elab.Structural.instInhabitedEqnInfo.default :
    EqnInfo
    Equations
      Instances For
        source
        instance Lean.Elab.Structural.instInhabitedEqnInfo :
        Inhabited EqnInfo
        Equations
          source
          opaque Lean.Elab.Structural.eqnInfoExt :
          MapDeclarationExtension EqnInfo
          source
          def Lean.Elab.Structural.registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) (fixedParamPerms : FixedParamPerms) :
          CoreM Unit
          Equations
            Instances For