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

Nat.Min.abs 16 --> Nat 16


Nat.Min.abs -4 --> Nat 4

Really only use this if you want the absolute value.

badLength list =
    List.length >> Nat.Min.abs


goodLength =
    List.foldl
        (\_ ->
            Nat.Min.addN nat1
                >> Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        )
        (Nat.N.toMin nat0)

If something like this isn't possible, use Nat.Min.intAtLeast!

Cap the Nat (Min ...) to at most a upper limit.

atMost5 : Nat (Min min) -> Nat (Min Nat5)
atMost5 =
    Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        >> Nat.Min.atMost (nat5 |> Nat.N.toMin) { min = nat0 }


atMost5 (nat12 |> Nat.N.toMin) --> Nat 5
atMost5 (nat3 |> Nat.N.toMin) --> Nat 3

A Nat (Min ...) from an Int; if the Int < minimum, minimum is returned.

9 |> Nat.Min.intAtLeast nat3 --> Nat 9


0 |> Nat.Min.intAtLeast nat3 --> Nat 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
        (\_ ->
            Nat.Min.addN nat1
                >> Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        )
        (Nat.N.toMin nat0)

If you want to handle the case < minimum yourself, use Nat.Min.isIntAtLeast.

If the Nat (Min ...) is lower than a lower limit, return the lower limit instead.

atLeast5 : Nat (Min min) -> Nat (Min Nat5)
atLeast5 =
    Nat.Min.atLeast (nat5 |> Nat.N.toMin)


atLeast5 (nat3 |> Nat.N.toMin) --> Nat 5
atLeast5 (nat12 |> Nat.N.toMin) --> Nat 12

If the Int >= a minimum, Just the Nat (Min minimum), else Nothing.

4 |> Nat.Min.isIntAtLeast nat5 --> Nothing


1234 |> Nat.Min.isIntAtLeast nat5 --> Just (Nat 1234)

Compare the Nat (Min ...) to a Nat (N ...). Is it greater, less or equal?

min ensures that the Nat (N ...) is bigger than the minimum.

present =
    Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        >> Nat.Min.is (nat18 |> Nat.N.toIn)
            { min = nat0 }
            { less = \age -> appropriateToy { age = age }
            , greater = \age -> appropriateExperience { age = age }
            , equal = \() -> bigPresent
            }


appropriateToy : { age : Nat (In Nat0 Nat17) } -> Toy


appropriateExperience : { age : Nat (Min Nat19) } -> Experience

Is the Nat (Min ...)

• equalOrGreater than a Nat or

• less?

factorial : Nat.Min min -> Nat.Min Nat1
factorial =
    Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        >> Nat.Min.isAtLeast (nat1 |> Nat.N.toIn)
            { min = nat0 }
            { less = \_ -> nat1 |> Nat.N.toMin
            , equalOrGreater =
                \atLeast1 ->
                    atLeast1
                        |> Nat.Min.mul
                            (factorial
                                (atLeast1 |> Nat.Min.subN nat1)
                            )
            }

Is the Nat (Min ...)

• equalOrLess than a Nat or

• greater?

goToU18Party : { age : Nat (In min Nat17) } -> List Snack

tryToGoToU18Party =
    Nat.Min.lowerMin (nat0 |> Nat.N.toIn)
        >> Nat.Min.isAtMost ( nat17, nat17 )
            { min = nat0 }
            { equalOrLess = \age -> Just (goToU18Party { age = age })
            , greater = Nothing
            }

Set the minimum lower.

[ Nat.N.toMin nat3, Nat.N.toMin nat4 ]

Elm complains:

But all the previous elements in the list are: Nat (Min Nat3)

[ Nat.N.toMin nat3
, Nat.N.toMin nat4 |> Nat.Min.lowerMin (nat3 |> Nat.N.toIn)
]

Add an exact Nat (N ...).

(nat5 |> Nat.N.toMin)
    |> Nat.Min.addN nat2
--> is of type Nat (Min Nat7)

Subtract an exact Nat.

(nat7 |> Nat.N.toMin)
    |> Nat.Min.subN nat2
--> is of type Nat (Min Nat5)

Add a Nat (Min ...). The second argument is the minimum if the added Nat (Min ...).

nat5
    |> Nat.N.toMin
    |> Nat.Min.add atLeast2 nat2
--> is of type Nat (Min Nat7)

Subtract a Nat (In ...). The second argument is the maximum if the subtracted Nat (In ...).

(nat5 |> Nat.N.toMin)
    |> Nat.Min.subIn inNat0To5 nat5
--> is of type Nat (Min Nat0)

Multiply by a Nat (Min ...) >= 1. we know that if a >= 1 → x * a >= x

five |> Nat.Min.mul two
--> Nat 10 of type Nat (Min Nat5)


two |> Nat.Min.mul five
--> Nat 10 of type Nat (Min Nat2)


two = nat2 |> Nat.N.toMin


five = nat5 |> Nat.N.toMin

Divide (//) by a Nat.Min. div 0 is impossible.

Nat.N.toMin nat7 |> Nat.Min.div (nat3 |> Nat.N.toMin)
--> Nat 2 of type Nat (Min Nat0)

The remainder after division. remainderBy 0 is impossible.

Nat.N.toMin nat7 |> Nat.Min.remainderBy (Nat.N.toMin nat3)
--> Nat 1 of type Nat (Min Nat0)

The Nat (Min ...) ^ a Nat (Min ...). We know that if a >= 1 → x ^ a >= x

five |> Nat.Min.toPower two
--> Nat 25 of type Nat (Min Nat5)


two |> Nat.Min.toPower five
--> Nat 25 of type Nat (Min Nat2)


two = nat2 |> Nat.N.toMin


five = nat5 |> Nat.N.toMin

Nat (Min ...)s from a first Nat (In ...) to a last Nat (Min ...).

An empty range cannot be constructed.