Cap the Nat (In ...) to at most a number.

nat5 |> NNat.toIn
    |> InNat.atMost nat10 { min = nat5 }
--> InNat 5


nat15 |> NNat.toIn |> InNat.lowerMin nat5
    |> InNat.atMost nat10 { min = nat5 }
--> Nat 10

min ensures that that number is at least the minimum.

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

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

present =
    InNat.lowerMin nat0
        >> InNat.is nat18
            { min = nat0 }
            { less = \age -> appropriateToy { age = age }
            , greater = \age -> appropriateExperience { age = age }
            , equal = \() -> bigPresent
            }


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


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

Compared to a range first to last, is the Nat (In ...)

• inRange

• greater than the last or

• less than the first?

justIfBetween3And10 =
    InNat.lowerMin nat0
        >> InNat.isInRange { first = nat3, last = nat10 }
            { min = nat0 }
            { less = \_ -> Nothing
            , greater = \_ -> Nothing
            , inRange = Just
            }

justIfBetween3And10 nat9
--> Just (Nat 9)

justIfBetween3And10 nat123
--> Nothing

Is the Nat (In ...)

• equalOrGreater than a Nat or

• less?

vote : { age : Nat (In (Nat18Plus orOlder) max) } -> Vote

tryToVote =
    InNat.lowerMin nat0
        >> InNat.isAtLeast nat18
            { min = nat0 }
            { less = Nothing --😓
            , equalOrGreater = \age -> Just (vote { age = age })
            }

Is the Nat (In ...)

• equalOrLess than a Nat or

• greater?

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

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

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

nat70 |> NNat.toIn
    |> InNat.addN nat7
--> is of type Nat (In Nat77 (Nat77Plus a))

Subtract a fixed Nat value.

nat7 |> NNat.toIn
    |> InNat.subN nat7
--> is of type Nat (In Nat0 a)

Use MinNat.subN if the maximum value is Infinity.

Add a Nat (In ...).

NNat.toIn nat3
    |> InNat.add between1And12 nat1 nat12
--> of type Nat (In Nat4 (Nat15Plus a))

Subtract a Nat (In ...).

The 2 following arguments are

• the minimum subtracted value
• the maximum subtracted value

If you don't have both at hand, use subLossy.

nat6 |> NNat.toIn
    |> InNat.sub between1And5 nat1 nat5
--> is of type Nat (In Nat1 (Nat5Plus a))

Subtract a Nat (In ..) without

• calculating the new minimum, the lowest possible value it can be after the subtraction is 0

nat6 |> NNat.toMin
    |> InNat.subLossy between1And5
--> is of type Nat (In Nat0 Infinity)

nat6 |> NNat.toIn
    |> InNat.subLossy between1And5
--> is of type Nat (In Nat0 (Nat6Plus a))

If you know the maximum subtracted value, use subLossyMax.

If you also know the minimum subtracted value, use sub.

Add a Nat (In ...), but

• keep the current minimum, instead of computing the exact value

• use Infinity as the maximum instead of computing the exact value

  atLeast5 |> MinNat.addLossy atLeast2 --> is of type Nat (ValueMin Nat5)

  atLeast2 |> MinNat.addLossy atLeast5 --> is of type Nat (ValueMin Nat2)

If you know the minimum and maximum added value, use add.

Make it fit into functions with require a higher maximum.

You should design type annotations as general as possible.

onlyAtMost18 : Nat (In min Nat18 maybeN)


onlyAtMost18 between3And8 --fine

But once you implement onlyAtMost18, you might use the value in onlyAtMost19.

onlyAtMost18 value =
    -- onlyAtMost19 value --error :(
    onlyAtMost19
        (value |> InNat.maxIs nat18 {- works :) -})

lowerMin is also handy in those situations.

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

in4To10 |> NNat.toMin
--> is of type Nat (ValueMin Nat4)

There is only 1 situation you should use this.

To make these the same type.

[ atLeast1, in1To10 ]

Elm complains:

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

[ atLeast1
, in1To10 |> InNat.toMin
]