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

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

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


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


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

Is the Nat (ValueMin ...)

• equalOrGreater than a Nat or

• less?

factorial : MinNat min -> MinNat Nat1
factorial =
    MinNat.lowerMin nat0
        >> MinNat.isAtLeast nat1
            { min = nat0 }
            { less = \_ -> nat1 |> InNat.toMin
            , equalOrGreater =
                \atLeast1 ->
                    atLeast1
                        |> MinNat.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 =
    MinNat.lowerMin nat0
        >> MinNat.isAtMost nat17
            { min = nat0 }
            { equalOrLess = \age -> Just (goToU18Party { age = age })
            , greater = Nothing
            }

Subtract an exact Nat (N ...).

(nat7 |> NNat.toMin)
    |> MinNat.subN nat2
--> is of type Nat (ValueMin Nat5)

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

nat5
    |> NNat.toMin
    |> MinNat.add atLeast2 nat2
--> is of type Nat (ValueMin Nat7)

If you have don't the minimum added value at hand, use InNat.addLossy.

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

atLeast6 |> MinNat.sub in0To5 nat5
--> is of type Nat (In Nat1 (Nat6Plus a))

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

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

nat70
    |> NNat.toMin
    |> InNat.addN nat7

Set the minimum lower.

[ atLeast3, atLeast4 ]

Elm complains:

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

[ atLeast3
, atLeast4 |> MinNat.lowerMin nat3
]

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

atLeast5 |> MinNat.toPower nat2
--> Nat 25 of type Nat (ValueMin Nat5)


atLeast2 |> MinNat.toPower nat5
--> Nat 25 of type Nat (ValueMin Nat2)

The remainder after division.

• % 0 is impossible
• x % d is at most x

atMost7 |> InNat.remainderBy nat3
--> Nat 1 of type Nat (In Nat0 (Nat7Plus a))

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

atLeast5  |> MinNat.mul nat2
--> Nat 10 of type Nat (ValueMin Nat5)


atLeast2 |> MinNat.mul nat5
--> Nat 10 of type Nat (ValueMin Nat2)

The maximum value of both factors can be Infinity.

Divide (//) by a Nat (In ...).

• / 0 is impossible

• x / d is at most x

atMost7
    |> InNat.div nat3
--> Nat 2 of type Nat (ValueIn Nat0 (Nat7Plus a))

If the Nat (In ...) is less than a number, return that number instead.

nat5 |> NNat.toIn
    |> InNat.atLeast nat10
--> Nat 10


nat15 |> NNat.toIn
    |> InNat.atLeast nat10
--> Nat 15