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
      @[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