Compare the Nat to a Nat (ArgN ...). Is it Greater, Less or Equal?

min ensures that the Nat (ArgN ...) is greater than the minimum.

giveAPresent { age } =
    case
        (age |> Nat.lowerMin nat0)
            |> MinNat.is nat18 { min = nat0 }
    of
        Nat.Less age ->
            toy { age = age }


        Nat.Greater age ->
            experience { age = age }


        Nat.Equal () ->
            bigPresent


toy : { age : Nat (ArgIn Nat0 Nat17 maybeN) } -> Toy


experience : { age : Nat (ArgIn Nat19 max maybeN) } -> Experience

Is the Nat

• EqualOrGreater than a Nat or

• Below a lower bound?

factorial : Nat (ArgIn min max maybeN) -> Nat (Min Nat1)
factorial =
    let
        factorialBody x =
            case x |> MinNat.isAtLeast nat1 { min = nat0 } of
                Nat.Below _ ->
                    MinNat.value nat1

                Nat.EqualOrGreater atLeast1 ->
                    Nat.mul atLeast1
                        (factorial
                            (atLeast1 |> MinNat.subN nat1)
                        )
    in
    Nat.lowerMin nat0 >> factorialBody

Is the Nat

• EqualOrLess than a Nat or

• Above?

goToU18Party : { age : Nat (ArgIn min Nat17 maybeN) } -> Snack

tryToGoToU18Party { age } =
    case
        (age |> Nat.lowerMin nat0)
            |> MinNat.isAtMost nat17 { min = nat0 }
    of
        EqualOrLess age ->
            Just (goToU18Party { age = age })

        Greater _ ->
            Nothing

Subtract an exact Nat (ArgN ...).

atLeast7 |> MinNat.subN nat2
--> : Nat (Min Nat5)

Add a Nat (ArgIn ...). The second argument is the minimum added value.

atLeast5 |> MinNat.add atLeast2 nat2
--> : Nat (Min Nat7)

Subtract a Nat (ArgIn ...). The second argument is the maximum of the subtracted Nat (ArgIn ...).

atLeast6 |> MinNat.sub between0And5 nat5
--> : Nat (Min Nat1)

If you have don't the maximum subtracted value at hand, use subLossy.

Add a fixed Nat (ArgN ...) value.

atLeast70 |> InNat.addN nat7
--> : Nat (Min Nat77)

Convert a Nat (ArgIn min ...) to a Nat (Min min).

between3And10 |> MinNat.value
--> : Nat (Min Nat4)

There is only 1 situation you should use this.

To make these the same type.

[ atLeast1, between1And10 ]

Elm complains:

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

[ atLeast1
, between1And10 |> MinNat.value
]

A Codec to serialize Nats with a lower bound.

import Serialize


serializeNaturalNumber :
    Serialize.Codec
        String
        (Nat (Min Nat0))
serializeNaturalNumber =
    MinNat.serialize nat0


encode : Nat (ArgIn min max maybeN) -> Bytes
encode =
    MinNat.value
        >> Serialize.encodeToBytes serializeNaturalNumber


decode :
    Bytes
    -> Result (Serialize.Error String) (Nat (Min Nat0))
decode =
    Serialize.decodeFromBytes serializeNaturalNumber