Documentation

Batteries.Data.Nat.Basic

source
๐Ÿ”ธ coverage
def Nat.recAuxOn {motive : Nat โ†’ Sort u_1} (t : Nat) (zero : motive 0) (succ : (n : Nat) โ†’ motive n โ†’ motive (n + 1)) :
motive t

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

Equations
Instances For
    source
    ๐Ÿ”ธ coverage
    @[irreducible]
    def Nat.strongRec {motive : Nat โ†’ Sort u_1} (ind : (n : Nat) โ†’ ((m : Nat) โ†’ m < n โ†’ motive m) โ†’ motive n) (t : Nat) :
    motive t

    Strong recursor for Nat

    Equations
    Instances For
      source
      ๐Ÿ”ธ coverage
      @[irreducible]
      def Nat.strongRecMeasure {ฮฑ : Sort u_1} (f : ฮฑ โ†’ Nat) {motive : ฮฑ โ†’ Sort u_2} (ind : (x : ฮฑ) โ†’ ((y : ฮฑ) โ†’ f y < f x โ†’ motive y) โ†’ motive x) (x : ฮฑ) :
      motive x

      Strong recursor via a Nat-valued measure

      Equations
      Instances For
        source
        ๐Ÿ”ธ coverage
        def Nat.recDiagAux {motive : Nat โ†’ Nat โ†’ Sort u_1} (zero_left : (n : Nat) โ†’ motive 0 n) (zero_right : (m : Nat) โ†’ motive m 0) (succ_succ : (m n : Nat) โ†’ motive m n โ†’ motive (m + 1) (n + 1)) (m n : Nat) :
        motive m n

        Simple diagonal recursor for Nat

        Equations
        Instances For
          source
          ๐Ÿ”ธ coverage
          def Nat.recDiag {motive : Nat โ†’ Nat โ†’ Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) โ†’ motive 0 n โ†’ motive 0 (n + 1)) (succ_zero : (m : Nat) โ†’ motive m 0 โ†’ motive (m + 1) 0) (succ_succ : (m n : Nat) โ†’ motive m n โ†’ motive (m + 1) (n + 1)) (m n : Nat) :
          motive m n

          Diagonal recursor for Nat

          Equations
          Instances For
            source
            ๐Ÿ”ธ coverage
            def Nat.recDiag.left {motive : Nat โ†’ Nat โ†’ Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) โ†’ motive 0 n โ†’ motive 0 (n + 1)) (n : Nat) :
            motive 0 n

            Left leg for Nat.recDiag

            Equations
            Instances For
              source
              ๐Ÿ”ธ coverage
              def Nat.recDiag.right {motive : Nat โ†’ Nat โ†’ Sort u_1} (zero_zero : motive 0 0) (succ_zero : (m : Nat) โ†’ motive m 0 โ†’ motive (m + 1) 0) (m : Nat) :
              motive m 0

              Right leg for Nat.recDiag

              Equations
              Instances For
                source
                ๐Ÿ”ธ coverage
                def Nat.recDiagOn {motive : Nat โ†’ Nat โ†’ Sort u_1} (m n : Nat) (zero_zero : motive 0 0) (zero_succ : (n : Nat) โ†’ motive 0 n โ†’ motive 0 (n + 1)) (succ_zero : (m : Nat) โ†’ motive m 0 โ†’ motive (m + 1) 0) (succ_succ : (m n : Nat) โ†’ motive m n โ†’ motive (m + 1) (n + 1)) :
                motive m n

                Diagonal recursor for Nat

                Equations
                Instances For
                  source
                  ๐Ÿ”ธ coverage
                  def Nat.casesDiagOn {motive : Nat โ†’ Nat โ†’ Sort 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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    ๐Ÿ”ธ coverage
                    def Nat.sqrt (n : Nat) :
                    Nat

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

                    Equations
                    Instances For
                      source
                      ๐Ÿ”ธ coverage
                      @[irreducible]
                      def Nat.sqrt.iter (n guess : Nat) :
                      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
                        source
                        ๐Ÿ”ธ coverage
                        @[inline]
                        def Nat.ofBits {n : Nat} (f : Fin n โ†’ Bool) :
                        Nat

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

                        Equations
                        Instances For
                          source
                          instance Nat.instNeZeroHPowOfNat_batteries {n : Nat} :
                          NeZero (n ^ 0)