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 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 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 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 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
                                    Instances For
                                      def Nat.sqrt (n : Nat) :

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

                                      Equations
                                        Instances For
                                          def Nat.sqrt.iter (n guess : Nat) :

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

                                          By default this well-founded recursion would be irreducible. This prevents use decide to resolve Nat.sqrt n for small values of n, so we mark this as @[semireducible].

                                          Equations
                                            Instances For
                                              @[inline]
                                              def Nat.ofBits {n : Nat} (f : Fin nBool) :

                                              Construct a natural number from a sequence of bits using little endian convention.

                                              Equations
                                                Instances For