Documentation

Batteries.Data.Nat.Basic

def Nat.recAuxOn {motive : NatSort u_1} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) :
motive t

Recursor identical to Nat.recOn but uses notations 0 for Nat.zero and ·+1 for Nat.succ

Equations
Instances For
    @[irreducible]
    def Nat.strongRec {motive : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) (t : Nat) :
    motive t

    Strong recursor for Nat

    Equations
    Instances For
      def Nat.strongRecOn (t : Nat) {motive : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
      motive t

      Strong recursor for Nat

      Equations
      Instances For
        @[irreducible]
        def Nat.strongRecMeasure {α : Sort u_1} (f : αNat) {motive : αSort u_2} (ind : (x : α) → ((y : α) → f y < f xmotive y)motive x) (x : α) :
        motive x

        Strong recursor via a Nat-valued measure

        Equations
        Instances For
          def Nat.recDiagAux {motive : NatNatSort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) (m : Nat) (n : Nat) :
          motive m n

          Simple diagonal recursor for Nat

          Equations
          Instances For
            def Nat.recDiag {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) (m : Nat) (n : Nat) :
            motive m n

            Diagonal recursor for Nat

            Equations
            Instances For
              def Nat.recDiag.left {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (n : Nat) :
              motive 0 n

              Left leg for Nat.recDiag

              Equations
              Instances For
                def Nat.recDiag.right {motive : NatNatSort u_1} (zero_zero : motive 0 0) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (m : Nat) :
                motive m 0

                Right leg for Nat.recDiag

                Equations
                Instances For
                  def Nat.recDiagOn {motive : NatNatSort u_1} (m : Nat) (n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) :
                  motive m n

                  Diagonal recursor for Nat

                  Equations
                  Instances For
                    def Nat.casesDiagOn {motive : NatNatSort u_1} (m : Nat) (n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) :
                    motive m n

                    Diagonal recursor for Nat

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def Nat.sqrt (n : Nat) :

                      Integer square root function. Implemented via Newton's method.

                      Equations
                      Instances For
                        @[irreducible]
                        def Nat.sqrt.iter (n : Nat) (guess : Nat) :

                        Auxiliary for sqrt. If guess is greater than the integer square root of n, returns the integer square root of n.

                        Equations
                        Instances For