Natural Numbers

Type signatures are provisional and may contain errors.

Basic Operations

isNat

(isNat n)
> n : a
> Bool

Checks if a value is a natural number.

isNat 5       == 1
isNat 0       == 1
isNat SOME    == 0
isNat b#hi    == 0

toNat

(toNat n)
> n : a
> Nat

Converts a value to a natural number. If the input is already a natural number, it returns it unchanged.

toNat 5       == 5
toNat 0       == 0
toNat SOME    == 0 ; Non-numbers become 0
toNat b#hi    == 0

times

(times f z n)
> f : (a > b)
> z : a
> n : Nat
> b

Applies a function f to an initial value z, x times.

times inc 0 3        == 3
times (mul 2) 1 4    == 16
times (add 2) 0 3    == 6

inc

(inc n)
> n : Nat
> Nat

Increments a natural number by 1.

inc 0      == 1
inc 5      == 6
inc 255    == 256

dec

(dec n)
> n : Nat
> Nat

Decrements a natural number by 1. Returns 0 if the input is 0.

dec 0      == 0
dec 1      == 0
dec 5      == 4
dec 256    == 255

add

(add x y)
> x : Nat
> y : Nat
> Nat

Adds two natural numbers.

add 3 4      == 7
add 0 5      == 5
add 255 1    == 256

sub

(sub x y)
> x : Nat
> y : Nat
> Nat

Subtracts one natural number from another. Returns 0 if the result would be negative.

sub 5 3      == 2
sub 3 5      == 0
sub 0 1      == 0
sub 256 1    == 255

mod

(mod x y)
> x : Nat
> y : Nat
> Nat

Calculates the modulus of two natural numbers.

mod 7 3     == 1
mod 6 3     == 0
mod 5 10    == 5
mod 0 5     == 0

mul

(mul x y)
> x : Nat
> y : Nat
> Nat

Multiplies two natural numbers.

mul 3 4      == 12
mul 0 5      == 0
mul 255 2    == 510

div

(div x y)
> x : Nat
> y : Nat
> Nat

Performs integer division on two natural numbers. Division by zero returns 0.

div 6 3     == 2
div 7 3     == 2
div 5 10    == 0
div 5 0     == 0

divMod

(divMod x y)
> x : Nat
> y : Nat
> SOME

Performs both division and modulus in one operation. Returns a tuple of (quotient, remainder).

divMod 7 3     == (0 2 1)
divMod 6 3     == (0 2 0)
divMod 5 10    == (0 0 5)
divMod 5 0     ; Division by zero, this will crash the REPL

isOne

(isOne n)
> x : Nat
> Nat

Checks if a natural number is equal to 1.

isOne 1    == 1
isOne 0    == 0
isOne 2    == 0

Bitwise Operations

lsh

(lsh x y)
> x : Nat
> y : Nat
> Nat

Left-shifts a natural number by a given amount.

lsh 1 3    == 8     ; 1 << 3 = 8
lsh 5 2    == 20    ; 5 << 2 = 20
lsh 8 1    == 16    ; 8 << 1 = 16

rsh

(rsh x y)
> x : Nat
> y : Nat
> Nat

Right-shifts a natural number by a given amount.

rsh 8 3     == 1    ; 8 >> 3 = 1
rsh 20 2    == 5    ; 20 >> 2 = 5
rsh 16 1    == 8    ; 16 >> 1 = 8

con

(con x y)
> x : Nat
> y : Nat
> Nat

Performs a bitwise AND operation on two natural numbers.

con 5 3      == 1    ; 0101 & 0011 = 0001
con 12 10    == 8    ; 1100 & 1010 = 1000
con 15 7     == 7    ; 1111 & 0111 = 0111

mix

(mix x y)
> x : Nat
> y : Nat
> Nat

Performs a bitwise XOR operation on two natural numbers.

mix 5 3      == 6    ; 0101 ^ 0011 = 0110
mix 12 10    == 6    ; 1100 ^ 1010 = 0110
mix 15 7     == 8    ; 1111 ^ 0111 = 1000

dis

(dis x y)
> x : Nat
> y : Nat
> Nat

Performs a bitwise OR operation on two natural numbers.

dis 5 3      == 7     ; 0101 | 0011 = 0111
dis 12 10    == 14    ; 1100 | 1010 = 1110
dis 15 7     == 15    ; 1111 | 0111 = 1111

pow

(pow b p)
> b : Nat
> p : Nat
> Nat

Raises a base to a power.

pow 2 3    == 8
pow 3 2    == 9
pow 5 0    == 1
pow 0 5    == 0

bex

(bex p)
> p : Nat
> Nat

Calculates 2 raised to a given power.

bex 3    == 8     ; 2^3 = 8
bex 5    == 32    ; 2^5 = 32
bex 0    == 1     ; 2^0 = 1

bix

(bix i n)
> i : Nat
> n : Nat
> Nat

Extracts a specific bit from a natural number.

bix 0 8    == 0    ; Least significant bit of 8 (1000) is 0
bix 3 8    == 1    ; 4th bit of 8 (1000) is 1
bix 2 7    == 1    ; 3rd bit of 7 (0111) is 1

natEql

(natEql x y)
> x : Nat
> y : Nat
> Bool

Checks if two natural numbers are equal.

natEql 5 5     == 1    ; TRUE
natEql 3 5     == 0    ; FALSE
natEql 0 0     == 1    ; TRUE

natCmp

(natCmp x y)
> x : Nat
> y : Nat
> Nat

Compares two natural numbers, returning an ordering result.

natCmp 3 5    == 0    ; LT
natCmp 5 3    == 2    ; GT
natCmp 4 4    == 1    ; EQ

Advanced Bitwise Operations

bitwise

(bitwise f x y)
> f : (Nat > Nat > Nat)
> x : Nat
> y : Nat
> Nat

Applies a bitwise operation to two natural numbers.

bitwise and 5 3    == 1    ; 0101 & 0011 = 0001
bitwise or  5 3    == 7    ; 0101 | 0011 = 0111
bitwise xor 5 3    == 6    ; 0101 ^ 0011 = 0110

natFold

(natFold f z n)
> f : (a > Nat > a)
> z : a
> n : Nat
> a

Folds a function over the bits of a natural number.

natFold add 0 5     == 2    ; Sum of bits in 5 (0101)
natFold or  0 10    == 1    ; OR of all bits in 10 (1010)

met

(met n)
> n : Nat
> Nat

Calculates the number of bits required to represent a natural number.

met 0      == 0
met 1      == 1
met 7      == 3
met 8      == 4
met 255    == 8
met 256    == 9

popCount

(popCount n)
> n : Nat
> Nat

Counts the number of set bits in a natural number.

popCount 0     == 0
popCount 1     == 1
popCount 7     == 3    ; 0111 has 3 set bits
popCount 15    == 4    ; 1111 has 4 set bits

trunc

(trunc w n)
> w : Nat
> n : Nat
> Nat

Truncates a natural number to a given bit width.

trunc 3 13    == 5
trunc 2 7     == 3     ; 7 (111) truncated to 2 bits is 3 (11)
trunc 4 15    == 15    ; 15 (1111) truncated to 4 bits is still 15

bitSlice

(bitSlice o w n)
> o : Nat
> w : Nat
> n : Nat
> Nat

Extracts a slice of bits from a natural number.

bitSlice 0 3 13    == 5
bitSlice 1 2 13    == 2    ; Bits 1-2 of 13 (1101) is 2 (10)
bitSlice 2 2 13    == 3    ; Bits 2-3 of 13 (1101) is 3 (11)

setBit

(setBit i n)
> i : Nat
> n : Nat
> Nat

Sets a specific bit in a natural number.

setBit 0 4    == 5
setBit 2 1    == 5    ; Set 3rd bit of 1 (001) to get 5 (101)
setBit 1 6    == 6    ; Setting already-set bit changes nothing

clearBit

(clearBit i n)
> i : Nat
> n : Nat
> Nat

Clears a specific bit in a natural number.

clearBit 0 5    == 4
clearBit 2 7    == 3    ; Clear 3rd bit of 7 (111) to get 3 (011)
clearBit 1 4    == 4    ; Clearing already-clear bit changes nothing

testBit

(testBit i n)
> i : Nat
> n : Nat
> Nat

Tests if a specific bit is set in a natural number.

testBit 0 5    == 1
testBit 1 5    == 0    ; 2nd bit of 5 (101) is not set
testBit 2 5    == 1    ; 3rd bit of 5 (101) is set

Miscellaneous

roundUp

(roundUp x y)
> x : Nat
> y : Nat
> Nat

Rounds a number up to the nearest multiple of another number.

```sire
roundUp 5 3    == 6
roundUp 6 3    == 6
roundUp 7 3    == 9
roundUp 0 3    == 0

even

(even n)
> n : Nat
> Bool

Checks if a natural number is even.

even 0     == 1
even 1     == 0
even 2     == 1
even 15    == 0

odd

(odd n)
> n : Nat
> Bool

Checks if a natural number is odd.

odd 0     == 0
odd 1     == 1
odd 2     == 0
odd 15    == 1

PreviousBits (Booleans)NextComparisons

Last updated 8 days ago