Documentation

Lean.Meta.RecursorInfo

Instances For
    Equations
      Instances For
        Equations
          Instances For
            Equations
              Instances For
                Equations
                  Instances For
                    Equations
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For
                                def Lean.Meta.mkRecursorInfo (declName : Name) (majorPos? : Option Nat := none) :
                                Equations
                                  Instances For