Documentation

Std.Data.Nat.Basic

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

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

Equations
Instances For
    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
      def Nat.casesAuxOn {motive : NatSort u_1} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) :
      motive t

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

      Equations
      Instances For
        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
            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
                      • Nat.casesDiagOn m n zero_zero zero_succ succ_zero succ_succ = Nat.recDiag zero_zero (fun x x_1 => zero_succ x) (fun x x_1 => succ_zero x) (fun x x_1 x_2 => succ_succ x x_1) m n
                      Instances For

                        Divisibility of natural numbers. a ∣ b (typed as \|) says that there is some c such that b = a * c.

                        Equations
                        def Nat.sum (l : List Nat) :

                        Sum of a list of natural numbers.

                        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 : 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