Nat.pred : Nat → Nat
Nat.pred : Nat → Nat

The predecessor of a natural number is one less than it. The predecessor of 0 is defined to be 0.

This definition is overridden in the compiler with an efficient implementation. This definition is the logical model.

Nat.add : Nat → Nat → Nat
Nat.add : Nat → Nat → Nat

Addition of natural numbers, typically used via the + operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Nat.sub : Nat → Nat → Nat
Nat.sub : Nat → Nat → Nat

Subtraction of natural numbers, truncated at 0. Usually used via the - operator.

If a result would be less than zero, then the result is zero.

This definition is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

• 5 - 3 = 2

• 8 - 2 = 6

• 8 - 8 = 0

• 8 - 20 = 0

Nat.mul : Nat → Nat → Nat
Nat.mul : Nat → Nat → Nat

Multiplication of natural numbers, usually accessed via the * operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Nat.div (x y : Nat) : Nat
Nat.div (x y : Nat) : Nat

Division of natural numbers, discarding the remainder. Division by 0 returns 0. Usually accessed via the / operator.

This operation is sometimes called “floor division.”

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

• 21 / 3 = 7

• 21 / 5 = 4

• 0 / 22 = 0

• 5 / 0 = 0

Nat.mod : Nat → Nat → Nat
Nat.mod : Nat → Nat → Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

Nat.mod is a wrapper around Nat.modCore that special-cases two situations, giving better definitional reductions:

• Nat.mod 0 m should reduce to m, for all terms m : Nat.

• Nat.mod n (m + n + 1) should reduce to n for concrete Nat literals n.

These reductions help Fin n literals work well, because the OfNat instance for Fin uses Nat.mod. In particular, (0 : Fin (n + 1)).val should reduce definitionally to 0. Nat.modCore can handle all numbers, but its definitional reductions are not as convenient.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

• 7 % 2 = 1

• 9 % 3 = 0

• 5 % 7 = 5

• 5 % 0 = 5

• show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl

• show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl

Nat.modCore (x y : Nat) : Nat
Nat.modCore (x y : Nat) : Nat

The modulo operator, which computes the remainder when dividing one natural number by another. Usually accessed via the % operator. When the divisor is 0, the result is the dividend rather than an error.

This is the core implementation of Nat.mod. It computes the correct result for any two closed natural numbers, but it does not have some convenient definitional reductions when the Nats contain free variables. The wrapper Nat.mod handles those cases specially and then calls Nat.modCore.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Nat.pow (m : Nat) : Nat → Nat
Nat.pow (m : Nat) : Nat → Nat

The power operation on natural numbers, usually accessed via the ^ operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Nat.log2 (n : Nat) : Nat
Nat.log2 (n : Nat) : Nat

Base-two logarithm of natural numbers. Returns ⌊max 0 (log₂ n)⌋.

This function is overridden at runtime with an efficient implementation. This definition is the logical model.

Examples:

• Nat.log2 0 = 0

• Nat.log2 1 = 0

• Nat.log2 2 = 1

• Nat.log2 4 = 2

• Nat.log2 7 = 2

• Nat.log2 8 = 3

Nat.min (n m : Nat) : Nat
Nat.min (n m : Nat) : Nat

Returns the lesser of two natural numbers. Usually accessed via Min.min.

Returns n if n ≤ m, or m if m ≤ n.

Examples:

• min 0 5 = 0

• min 4 5 = 4

• min 4 3 = 3

• min 8 8 = 8

Nat.max (n m : Nat) : Nat
Nat.max (n m : Nat) : Nat

Returns the greater of two natural numbers. Usually accessed via Max.max.

Returns m if n ≤ m, or n if m ≤ n.

Examples:

• max 0 5 = 5

• max 4 5 = 5

• max 4 3 = 4

• max 8 8 = 8

Nat.gcd (m n : Nat) : Nat
Nat.gcd (m n : Nat) : Nat

Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the largest natural number that evenly divides both.

In particular, the GCD of a number and 0 is the number itself.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here is the logical model.

Examples:

• Nat.gcd 10 15 = 5

• Nat.gcd 0 5 = 5

• Nat.gcd 7 0 = 7

Nat.lcm (m n : Nat) : Nat
Nat.lcm (m n : Nat) : Nat

The least common multiple of m and n is the smallest natural number that's evenly divisible by both m and n. Returns 0 if either m or n is 0.

Examples:

• Nat.lcm 9 6 = 18

• Nat.lcm 9 3 = 9

• Nat.lcm 0 3 = 0

• Nat.lcm 3 0 = 0

Nat.isPowerOfTwo (n : Nat) : Prop
Nat.isPowerOfTwo (n : Nat) : Prop

A natural number n is a power of two if there exists some k : Nat such that n = 2 ^ k.

Nat.nextPowerOfTwo (n : Nat) : Nat
Nat.nextPowerOfTwo (n : Nat) : Nat

Returns the least power of two that's greater than or equal to n.

Examples:

• Nat.nextPowerOfTwo 0 = 1

• Nat.nextPowerOfTwo 1 = 1

• Nat.nextPowerOfTwo 2 = 2

• Nat.nextPowerOfTwo 3 = 4

• Nat.nextPowerOfTwo 5 = 8

Nat.repeat.{u} {α : Type u} (f : α → α) (n : Nat) (a : α) : α
Nat.repeat.{u} {α : Type u} (f : α → α)
  (n : Nat) (a : α) : α

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

Examples:

• Nat.repeat f 3 a = f <| f <| f <| a

• Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"

Nat.repeatTR.{u} {α : Type u} (f : α → α) (n : Nat) (a : α) : α
Nat.repeatTR.{u} {α : Type u} (f : α → α)
  (n : Nat) (a : α) : α

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

This is a tail-recursive version of Nat.repeat that's used at runtime.

Examples:

• Nat.repeatTR f 3 a = f <| f <| f <| a

• Nat.repeatTR (· ++ "!") 4 "Hello" = "Hello!!!!"

Nat.fold.{u} {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α)
  (init : α) : α
Nat.fold.{u} {α : Type u} (n : Nat)
  (f : (i : Nat) → i < n → α → α)
  (init : α) : α

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

Examples:

• Nat.fold 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))

• Nat.fold 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]

• Nat.fold 0 (fun i _ xs => xs.push i) #[] = #[]

Nat.foldTR.{u} {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α)
  (init : α) : α
Nat.foldTR.{u} {α : Type u} (n : Nat)
  (f : (i : Nat) → i < n → α → α)
  (init : α) : α

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

This is a tail-recursive version of Nat.fold that's used at runtime.

Examples:

• Nat.foldTR 3 f init = (init |> f 0 (by simp) |> f 1 (by simp) |> f 2 (by simp))

• Nat.foldTR 4 (fun i _ xs => xs.push i) #[] = #[0, 1, 2, 3]

• Nat.foldTR 0 (fun i _ xs => xs.push i) #[] = #[]

Nat.foldM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m] (n : Nat)
  (f : (i : Nat) → i < n → α → m α) (init : α) : m α
Nat.foldM.{u, v} {α : Type u}
  {m : Type u → Type v} [Monad m]
  (n : Nat)
  (f : (i : Nat) → i < n → α → m α)
  (init : α) : m α

Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in increasing order.

Nat.foldRev.{u} {α : Type u} (n : Nat) (f : (i : Nat) → i < n → α → α)
  (init : α) : α
Nat.foldRev.{u} {α : Type u} (n : Nat)
  (f : (i : Nat) → i < n → α → α)
  (init : α) : α

Iterates the application of a function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

Examples:

• Nat.foldRev 3 f init = (f 0 (by simp) <| f 1 (by simp) <| f 2 (by simp) init)

• Nat.foldRev 4 (fun i _ xs => xs.push i) #[] = #[3, 2, 1, 0]

• Nat.foldRev 0 (fun i _ xs => xs.push i) #[] = #[]

Nat.foldRevM.{u, v} {α : Type u} {m : Type u → Type v} [Monad m]
  (n : Nat) (f : (i : Nat) → i < n → α → m α) (init : α) : m α
Nat.foldRevM.{u, v} {α : Type u}
  {m : Type u → Type v} [Monad m]
  (n : Nat)
  (f : (i : Nat) → i < n → α → m α)
  (init : α) : m α

Iterates the application of a monadic function f to a starting value init, n times. At each step, f is applied to the current value and to the next natural number less than n, in decreasing order.

Nat.forM.{u_1} {m : Type → Type u_1} [Monad m] (n : Nat)
  (f : (i : Nat) → i < n → m Unit) : m Unit
Nat.forM.{u_1} {m : Type → Type u_1}
  [Monad m] (n : Nat)
  (f : (i : Nat) → i < n → m Unit) :
  m Unit

Executes a monadic action on all the numbers less than some bound, in increasing order.

Example:

0 1 2 3 4 #eval Nat.forM 5 fun i _ => IO.println i 0 1 2 3 4

Nat.forRevM.{u_1} {m : Type → Type u_1} [Monad m] (n : Nat)
  (f : (i : Nat) → i < n → m Unit) : m Unit
Nat.forRevM.{u_1} {m : Type → Type u_1}
  [Monad m] (n : Nat)
  (f : (i : Nat) → i < n → m Unit) :
  m Unit

Executes a monadic action on all the numbers less than some bound, in decreasing order.

Example:

4 3 2 1 0 #eval Nat.forRevM 5 fun i _ => IO.println i 4 3 2 1 0

Nat.all (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool
Nat.all (n : Nat)
  (f : (i : Nat) → i < n → Bool) : Bool

Checks whether f returns true for every number strictly less than a bound.

Examples:

• Nat.all 4 (fun i _ => i < 5) = true

• Nat.all 7 (fun i _ => i < 5) = false

• Nat.all 7 (fun i _ => i % 2 = 0) = false

• Nat.all 1 (fun i _ => i % 2 = 0) = true

Nat.allTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool
Nat.allTR (n : Nat)
  (f : (i : Nat) → i < n → Bool) : Bool

Checks whether f returns true for every number strictly less than a bound.

This is a tail-recursive equivalent of Nat.all that's used at runtime.

Examples:

• Nat.allTR 4 (fun i _ => i < 5) = true

• Nat.allTR 7 (fun i _ => i < 5) = false

• Nat.allTR 7 (fun i _ => i % 2 = 0) = false

• Nat.allTR 1 (fun i _ => i % 2 = 0) = true

Nat.any (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool
Nat.any (n : Nat)
  (f : (i : Nat) → i < n → Bool) : Bool

Checks whether there is some number less that the given bound for which f returns true.

Examples:

• Nat.any 4 (fun i _ => i < 5) = true

• Nat.any 7 (fun i _ => i < 5) = true

• Nat.any 7 (fun i _ => i % 2 = 0) = true

• Nat.any 1 (fun i _ => i % 2 = 1) = false

Nat.anyTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool
Nat.anyTR (n : Nat)
  (f : (i : Nat) → i < n → Bool) : Bool

Checks whether there is some number less that the given bound for which f returns true.

This is a tail-recursive equivalent of Nat.any that's used at runtime.

Examples:

• Nat.anyTR 4 (fun i _ => i < 5) = true

• Nat.anyTR 7 (fun i _ => i < 5) = true

• Nat.anyTR 7 (fun i _ => i % 2 = 0) = true

• Nat.anyTR 1 (fun i _ => i % 2 = 1) = false

Nat.allM.{u_1} {m : Type → Type u_1} [Monad m] (n : Nat)
  (p : (i : Nat) → i < n → m Bool) : m Bool
Nat.allM.{u_1} {m : Type → Type u_1}
  [Monad m] (n : Nat)
  (p : (i : Nat) → i < n → m Bool) :
  m Bool

Checks whether the monadic predicate p returns true for all numbers less that the given bound. Numbers are checked in increasing order until p returns false, after which no further are checked.

Nat.anyM.{u_1} {m : Type → Type u_1} [Monad m] (n : Nat)
  (p : (i : Nat) → i < n → m Bool) : m Bool
Nat.anyM.{u_1} {m : Type → Type u_1}
  [Monad m] (n : Nat)
  (p : (i : Nat) → i < n → m Bool) :
  m Bool

Checks whether there is some number less that the given bound for which the monadic predicate p returns true. Numbers are checked in increasing order until p returns true, after which no further are checked.

Nat.toUInt8 (n : Nat) : UInt8
Nat.toUInt8 (n : Nat) : UInt8

Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt8 5 = 5

• Nat.toUInt8 255 = 255

• Nat.toUInt8 256 = 0

• Nat.toUInt8 259 = 3

• Nat.toUInt8 32770 = 2

Nat.toUInt16 (n : Nat) : UInt16
Nat.toUInt16 (n : Nat) : UInt16

Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt16 5 = 5

• Nat.toUInt16 255 = 255

• Nat.toUInt16 32770 = 32770

• Nat.toUInt16 65537 = 1

Nat.toUInt32 (n : Nat) : UInt32
Nat.toUInt32 (n : Nat) : UInt32

Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt32 5 = 5

• Nat.toUInt32 65_539 = 65_539

• Nat.toUInt32 4_294_967_299 = 3

Nat.toUInt64 (n : Nat) : UInt64
Nat.toUInt64 (n : Nat) : UInt64

Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:

• Nat.toUInt64 5 = 5

• Nat.toUInt64 65539 = 65539

• Nat.toUInt64 4_294_967_299 = 4_294_967_299

• Nat.toUInt64 18_446_744_073_709_551_620 = 4

Nat.toUSize (n : Nat) : USize
Nat.toUSize (n : Nat) : USize

Converts an arbitrary-precision natural number to an unsigned word-sized integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Nat.toInt8 (n : Nat) : Int8
Nat.toInt8 (n : Nat) : Int8

Converts a natural number to an 8-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt8 53 = 53

• Nat.toInt8 127 = 127

• Nat.toInt8 128 = -128

• Nat.toInt8 255 = -1

Nat.toInt16 (n : Nat) : Int16
Nat.toInt16 (n : Nat) : Int16

Converts a natural number to a 16-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt16 127 = 127

• Nat.toInt16 32767 = 32767

• Nat.toInt16 32768 = -32768

• Nat.toInt16 32770 = -32766

Nat.toInt32 (n : Nat) : Int32
Nat.toInt32 (n : Nat) : Int32

Converts a natural number to a 32-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt32 127 = 127

• Nat.toInt32 32770 = 32770

• Nat.toInt32 2_147_483_647 = 2_147_483_647

• Nat.toInt32 2_147_483_648 = -2_147_483_648

Nat.toInt64 (n : Nat) : Int64
Nat.toInt64 (n : Nat) : Int64

Converts a natural number to a 64-bit signed integer, wrapping around to negative numbers on overflow.

Examples:

• Nat.toInt64 127 = 127

• Nat.toInt64 2_147_483_648 = 2_147_483_648

• Nat.toInt64 9_223_372_036_854_775_807 = 9_223_372_036_854_775_807

• Nat.toInt64 9_223_372_036_854_775_808 = -9_223_372_036_854_775_808

• Nat.toInt64 18_446_744_073_709_551_618 = 0

Nat.toISize (n : Nat) : ISize
Nat.toISize (n : Nat) : ISize

Converts an arbitrary-precision natural number to a word-sized signed integer, wrapping around on overflow.

This function is overridden at runtime with an efficient implementation.

Nat.toFloat (n : Nat) : Float
Nat.toFloat (n : Nat) : Float

Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite floating-point value if the range of Float is exceeded.

Nat.toFloat32 (n : Nat) : Float32
Nat.toFloat32 (n : Nat) : Float32

Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite floating-point value if the range of Float32 is exceeded.

Nat.isValidChar (n : Nat) : Prop
Nat.isValidChar (n : Nat) : Prop

A Nat denotes a valid Unicode code point if it is less than 0x110000 and it is also not a surrogate code point (the range 0xd800 to 0xdfff inclusive).

Nat.repr (n : Nat) : String
Nat.repr (n : Nat) : String

Converts a natural number to its decimal string representation.

Nat.toDigits (base n : Nat) : List Char
Nat.toDigits (base n : Nat) : List Char

Returns the decimal representation of a natural number as a list of digit characters in the given base. If the base is greater than 16 then '*' is returned for digits greater than 0xf.

Examples:

• Nat.toDigits 10 0xff = ['2', '5', '5']

• Nat.toDigits 8 0xc = ['1', '4']

• Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e']

• Nat.toDigits 80 200 = ['2', '*']

Nat.digitChar (n : Nat) : Char
Nat.digitChar (n : Nat) : Char

Returns a single digit representation of n, which is assumed to be in a base less than or equal to 16. Returns '*' if n > 15.

Examples:

• Nat.digitChar 5 = '5'

• Nat.digitChar 12 = 'c'

• Nat.digitChar 15 = 'f'

• Nat.digitChar 16 = '*'

• Nat.digitChar 85 = '*'