Documentation

Lean.AuxRecursor

Equations
Instances For
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                def Lean.mkRecOnName (indDeclName : Lake.Name) :
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      def Lean.mkBelowName (indDeclName : Lake.Name) :
                      Equations
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            @[export lean_is_aux_recursor]
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                Instances For
                                  @[export lean_is_no_confusion]
                                  Equations
                                  Instances For