Documentation

Lean.Meta.RecursorInfo

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • info.numParams = info.paramsPos.length
    Instances For
      Equations
      • info.numIndices = info.indicesPos.length
      Instances For
        Equations
        • info.motivePos = info.numParams
        Instances For
          Equations
          • info.firstIndexPos = info.majorPos - info.numIndices
          Instances For
            Equations
            Instances For
              Equations
              • info.numMinors = info.numArgs - info.motivePos - 1 - (info.majorPos + 1 - info.firstIndexPos)
              Instances For
                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.
                Instances For
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For