NatFrom min meaning a natural number which is at least min.

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

Any natural number

MinNat Nat0

A number, bigger than 4

MinNat Nat5

Cap the MinNat to at most a upper limit.

The absolute value of an Int, which is at least Nat0.

MinNat.abs 16 --> MinNat 16


MinNat.abs -4 --> MinNat 4

Really only use this if you want the absolute value.

badLength list =
    List.length >> MinNat.abs


goodLength =
    List.foldl
        (\_ -> MinNat.addN nat1 >> MinNat.lowerMin nat0)
        (MinNat.n nat0)

If something like this isn't possible, use [MinNat.intAtLeast][MinNat#intAtLeast] nat0!

A MinNat from an Int; if the Int < minimum, minimum is returned.

9 |> MinNat.intAtLeast nat3 --> MinNat 9


0 |> MinNat.intAtLeast nat3 --> MinNat 3

You can also use this if you know an Int must be at least minimum.

But avoid it if you can do better, like

goodLength =
    List.foldl
        (\_ -> MinNat.addN nat1 >> MinNat.lowerMin nat0)
        (MinNat.n nat0)

If you want to handle the case < minimum yourself, use [MinNat.isIntAtLeast][MinNat#isIntAtLeast].

If the Int >= a minimum, Just the MinNat, else Nothing.

4 |> MinNat.isIntAtLeast nat5 --> Nothing


1234 |> MinNat.isIntAtLeast nat5 --> Just (NatIn 1234)

Compared to an exact NNat.

Is the MinNat

• equalOrGreater than a NNat or

• less?

factorialHelp : MinNat min -> MinNat Nat1
factorialHelp =
    MinNat.lowerMin nat0
        >> MinNat.isAtLeast nat1
            { min = nat0 }
            { less = \_ -> MinNat.n nat1
            , equalOrGreater =
                \oneOrGreater ->
                    oneOrGreater
                        |> MinNat.mul
                            (factorialHelp
                                (oneOrGreater |> MinNat.subN nat1)
                            )
            }

Is the MinNat

• equalOrLess than a NNat or

• greater?

Convert a MinNat to an Int.

MinNat.n nat4 |> MinNat.toInt --> 4


compare a b =
    compare (MinNat.toInt a) (MinNat.toInt b)

Convert an exact NNat n to a MinNat n (n + a).

MinNat.n nat4
--> is of type MinNat Nat4 (Nat4Plus a)

Set the minimum lower.

Add an exact NNat.

(nat5 |> MinNat.n)
    |> MinNat.addN nat2
--> MinNat 7

Subtract an exact NNat.

(nat7 |> MinNat.n)
    |> MinNat.subN nat2
--> MinNat 5

Add a MinNat. The second argument is the minimum if the added MinNat.

(nat5 |> MinNat.n)
    |> MinNat.add atLeast2 nat2

Subtract a InNat. The second argument is the maximum if the subtracted InNat.

(nat5 |> MinNat.n)
    |> MinNat.subIn inNat0To5 itsMaximum

Multiply by a MinNat >= 1. We can't compute the highest possiblenew minimum, we only know that if a >= 1 → x * a >= x

five |> MinNat.mul two
--> MinNat 10, but the type is MinNat Nat5


two |> MinNat.mul five
--> MinNat 10, but the type is MinNat Nat2


two = nat2 |> MinNat.n


five = nat5 |> MinNat.n

Divide (//) by a MinNat. div 0 is impossible.

MinNat.n nat7 |> MinNat.div (MinNat.n nat3)
--> MinNat 2 of type MinNat Nat0

The remainder after division. remainderBy 0 is impossible.

MinNat.n nat7 |> MinNat.remainderBy (MinNat.n nat3)
--> MinNat Nat0

The MinNat ^ a MinNat. We can't compute the highest possible new minimum, we only know that if a >= 1 → x ^ a >= x

five |> MinNat.toPower two
--> MinNat 25, but the type is MinNat Nat5


two |> MinNat.mul five
--> MinNat 25, but the type is MinNat Nat2


two = nat2 |> MinNat.n


five = nat5 |> MinNat.n

MinNats from a first InNat to a last MinNat.