Min minimum: At least minimum.

   ↓ minimum
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓...

Any natural number:

Nat (Min Nat0)

A number, at least 5:

Nat (Min Nat5)

In minimum maximum: Somewhere within a minimum & maximum.

   ↓ minimum   ↓ maximum
⨯ [✓ ✓ ✓ ✓ ✓ ✓ ✓] ⨯ ⨯ ⨯...

Note: maximum >= minimum for every existing Nat (In ...):

percent : Nat (In minimum Nat100)

→ minimum <= Nat100

Just the exact number.

Only useful in function annotations.

byte : Arr (Only Nat8) Bit -> Byte

→ A given Arr must have exact 8 Bits.

repeat : Nat (Only n) -> element -> Arr (Only n)


repeat (Nat.N.toIn nat6) "ok"
--> Arr (Only Nat6)

→ repeating an element n times will give you a Arr of n elements.

→ Every In NatXYZ (NatXYZPlus a) is also a Only NatXYZ, but not the other way around

The actual value is present in the type.

Looking at the type

nat0 :
    -- natural number
    Nat
        (N
            -- 0 is the exact value at compile time
            Nat0
            (-- 0 as a difference is a - a & b - b
             IsBoth a To a And b To b
            )
        )

• use Is a To b to describe a difference between two values

  • An example is Nat.Min.addN

    addN :
        Nat (N added (Is min To sumMin))
        -> Nat (Min min)
        -> Nat (Min sumMin)

• use IsBoth a To b And c To d to describe 2 differences

  • An example is Nat.In.addN

    addN :
        Nat (N added (IsBoth min To sumMin And max To sumMax))
        -> Nat (In min max)
        -> Nat (In sumMin sumMax)

If you only want to ensure that it is within a minimum (& maximum), Min or In is the right choice! This is the better choice for most calculations.

b - a.

Is a To (Nat1Plus a)

would describe a difference of 1.

An example is Nat.Min.addN

addN :
    Nat (N added (Is min To sumMin))
    -> Nat (Min min)
    -> Nat (Min sumMin)

b - a & d - c.

IsBoth a To (Nat1Plus a) And b To (Nat1Plus b)

would describe a difference of 1.

An example is Nat.In.addN

addN :
    Nat (N added (IsBoth min To sumMin And max To sumMax))
    -> Nat (In min max)
    -> Nat (In sumMin sumMax)

No special meaning.

IsBoth a To b And c To d

No special meaning.

Is a To b