Subtract an exact Nat (N ...).

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

Use subMax if you want to subtract a Nat that isn't a Nat (N ...).

Add an exact Nat (N ...) value.

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

Use addMin if you want to add a Nat that isn't a Nat (N ...).

Subtract a Nat that isn't a Nat (N ...). The second argument is the maximum of the subtracted Nat.

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

Add a Nat. The second argument is the minimum added value. Use add to add exact numbers.

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

Is the Nat LessOrEqualOrGreater than a given number?

lowest can be a number <= the minimum.

giveAPresent { age } =
    case age |> MinNat.is nat18 { lowest = nat0 } of
        Nat.Less younger ->
            toy { age = younger }


        Nat.Greater older ->
            book { age = older }


        Nat.Equal _ ->
            bigPresent


toy : { age : Nat (ArgIn min_ Nat17 ifN_) } -> Toy


book :
    { age : Nat (ArgIn (Nat19 minMinus19_) max_ ifN_) }
    -> Book

Is the Nat BelowOrAtLeast a given number?

factorial : Nat (ArgIn min_ max_ ifN_) -> Nat (Min Nat1)
factorial =
    factorialBody


factorialBody : Nat (ArgIn min_ max_ ifN_) -> Nat (Min Nat1)
factorialBody =
    case x |> MinNat.isAtLeast nat1 { lowest = nat0 } of
        Nat.Below _ ->
            Nat.toMin nat1


        Nat.EqualOrGreater atLeast1 ->
            Nat.mul atLeast1
                (factorial
                    (atLeast1 |> MinNat.sub nat1)
                )

Is the Nat AtMostOrAbove a given number?

goToU18Party : { age : Nat (ArgIn min_ Nat17 ifN_) } -> Snack


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


        Greater _ ->
            Nothing

Return the given number if the Nat is less.

nat5 |> MinNat.atLeast nat10
--> Nat 10 : Nat (Min Nat10)


atLeast5 |> MinNat.atLeast nat10
--> : Nat (Min Nat10)

A Codec to serialize Nats with a lower bound.

import Serialize exposing (Codec)


serializeNaturalNumber : Codec String (Nat (Min Nat0))
serializeNaturalNumber =
    MinNat.serialize nat0
        -- if we just want a simple error string
        |> Serialize.mapError MinNat.errorToString

The encode/decode functions can be extracted if needed.

encodeNaturalNumber : Nat (ArgIn min_ max_ ifN_) -> Bytes
encodeNaturalNumber =
    Nat.lowerMin nat0
        >> Nat.toMin
        >> Serialize.encodeToBytes serializeNaturalNumber


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

An error for when a decoded int is less than the expected minimum. You can transform it into

• a message: errorToString
• an InNat.Error: generalizeError

See serialize.

Convert an Error to a readable message.

{ expected = { atLeast = nat11 }
, actual = 10
}
    |> MinNat.errorToString
--> "expected an int >= 11 but the actual int was 10"

(example won't compile because nat11 isn't of type Nat (Min Nat0))

Equivalent to

error
    |> MinNat.generalizeError
    |> InNat.errorToString

Use the same error type as InNat.

import Serialize exposing (Codec)


Serialize.mapError MinNat.generalizeError
--> : Codec MinNat.Error a -> Codec InNat.Error a

Use this if you serialize InNat together with MinNat:

Serialize.tuple
    (MinNat.serialize nat0)
    (InNat.serialize nat0 nat99)
--> error : `Codec`s have different custom errors


Serialize.tuple
    (MinNat.serialize nat0
        |> Serialize.mapError MinNat.generalizeError
    )
    (InNat.serialize nat0 nat99)
--> Codec
-->     InNat.Error
-->     ( Nat (Min Nat0), Nat (In Nat0 (Nat99Plus a_)) )

Note: there's also errorToString.