Documentation

Lean.Elab.PreDefinition.PartialFixpoint.Eqns

def Lean.Elab.PartialFixpoint.registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedParamPerms : FixedParamPerms) (fixpointType : Array PartialFixpointType) :
Equations
    Instances For

      Generate the "unfold" lemma for declName.

      Equations
        Instances For
          Equations
            Instances For
              Equations
                Instances For
                  Equations
                    Instances For