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

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

present =
    Nat.lowerMin nat0
        >> MinNat.is nat18
            { min = nat0 }
            { less = \age -> toy { age = age }
            , greater = \age -> experience { age = age }
            , equal = \() -> bigPresent
            }


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


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

Is the Nat (ValueMin ...)

• equalOrGreater than a Nat or

• less?

factorial : Nat (In min max maybeN) -> Nat (ValueMin Nat1)
factorial =
    Nat.lowerMin nat0
        >> MinNat.isAtLeast nat1
            { min = nat0 }
            { less = \_ -> nat1 |> MinNat.value
            , equalOrGreater =
                \atLeast1 ->
                    atLeast1
                        |> Nat.mul
                            (factorial
                                (atLeast1 |> MinNat.subN nat1)
                            )
            }

Is the Nat (ValueMin ...)

• equalOrLess than a Nat or

• greater?

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

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

Subtract an exact Nat (N ...).

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

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

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

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

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

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

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

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

Convert a Nat (In min ...) to a Nat (ValueMin min).

between3And10 |> MinNat.value
--> : Nat (ValueMin 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 (ValueMin Nat1)

[ atLeast1
, between1And10 |> MinNat.value
]

A Codec to serialize Nats with a lower bound.

import Serialize


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


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


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