This module exists to provide the very basic UInt8
etc. definitions required for
Init.Data.Char.Basic
and Init.Data.Array.Basic
. These are very important as they are used in
meta code that is then (transitively) used in Init.Data.UInt.Basic
and Init.Data.BitVec.Basic
.
This file thus breaks the import cycle that would be created by this dependency.
Converts a natural number to an 8-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt8.ofNat 5 = 5
UInt8.ofNat 255 = 255
UInt8.ofNat 256 = 0
UInt8.ofNat 259 = 3
UInt8.ofNat 32770 = 2
Equations
Instances For
Converts a natural number to an 8-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^8 - 1
for natural numbers greater than or equal to 2^8
.
Equations
Instances For
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
Equations
Instances For
Converts an 8-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts a UInt16
into the corresponding Fin UInt16.size
.
Equations
Instances For
Converts a natural number to a 16-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt16.ofNat 5 = 5
UInt16.ofNat 255 = 255
UInt16.ofNat 32770 = 32770
UInt16.ofNat 65537 = 1
Equations
Instances For
Converts a natural number to a 16-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^16 - 1
for natural numbers greater than or equal to 2^16
.
Equations
Instances For
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
Equations
Instances For
Converts a 16-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 16-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 8-bit unsigned integers to 16-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts a UInt32
into the corresponding Fin UInt32.size
.
Equations
Instances For
Converts a natural number to a 32-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt32.ofNat 5 = 5
UInt32.ofNat 65539 = 65539
UInt32.ofNat 4_294_967_299 = 3
Equations
Instances For
Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than 2^32
.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts a natural number to a 32-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^32 - 1
for natural numbers greater than or equal to 2^32
.
Equations
Instances For
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
Equations
Instances For
Converts a 32-bit unsigned integer to an 8-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 32-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 8-bit unsigned integers to 32-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 16-bit unsigned integers to 32-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts a UInt64
into the corresponding Fin UInt64.size
.
Equations
Instances For
Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.
This function is overridden at runtime with an efficient implementation.
Examples:
UInt64.ofNat 5 = 5
UInt64.ofNat 65539 = 65539
UInt64.ofNat 4_294_967_299 = 4_294_967_299
UInt64.ofNat 18_446_744_073_709_551_620 = 4
Equations
Instances For
Converts a natural number to a 64-bit unsigned integer, returning the largest representable value if the number is too large.
Returns 2^64 - 1
for natural numbers greater than or equal to 2^64
.
Equations
Instances For
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
Equations
Instances For
Converts a 64-bit unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 64-bit unsigned integers to 8-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 64-bit unsigned integers to 16-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 64-bit unsigned integers to 32-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 8-bit unsigned integers to 64-bit unsigned integers.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 16-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Converts 32-bit unsigned integers to 64-bit unsigned integers. Wraps around on overflow.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
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.
Equations
Instances For
Converts a natural number to USize
, returning the largest representable value if the number is too
large.
Returns USize.size - 1
, which is 2^64 - 1
or 2^32 - 1
depending on the platform, for natural
numbers greater than or equal to USize.size
.
Equations
Instances For
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.
Equations
Instances For
Converts a word-sized unsigned integer to an arbitrary-precision natural number.
This function is overridden at runtime with an efficient implementation.
Equations
Instances For
Decides whether one word-sized unsigned integer is strictly less than another. Usually accessed via
the DecidableLT USize
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (6 : USize) < 7 then "yes" else "no") = "yes"
(if (5 : USize) < 5 then "yes" else "no") = "no"
show ¬((7 : USize) < 7) by decide
Equations
Decides whether one word-sized unsigned integer is less than or equal to another. Usually accessed
via the DecidableLE USize
instance.
This function is overridden at runtime with an efficient implementation.
Examples:
(if (15 : USize) ≤ 15 then "yes" else "no") = "yes"
(if (15 : USize) ≤ 5 then "yes" else "no") = "no"
(if (5 : USize) ≤ 15 then "yes" else "no") = "yes"
show (7 : USize) ≤ 7 by decide