MinNat

2 situations where you use these operations instead of the ones in Nat or InNat:

Your value is of type Nat (ValueMin ...)

nat3 |> Nat.mul nat3
--> Nat (ValueMin Nat3)

The maximum is a type variable

divideBy : Nat (In (Nat1Plus minMinus1) max maybeN) -> --...
divideBy atLeast1 =
    --...

compare

is :

Nat

(In

(Nat1Plus triedMinus1)

(Nat1Plus atLeastTriedMinus1)

triedMaybeN

)

-> { min : Nat (N min (Is minToTriedMinus1 To triedMinus1) x) }

-> { equal : () -> result

, less : Nat (In min atLeastTriedMinus1 maybeN) -> result

, greater : Nat (ValueMin (Nat2Plus triedMinus1)) -> result

}

-> Nat (In min max maybeN)

-> result

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 =
    MNat.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

isAtLeast :

Nat (In triedMin (Nat1Plus triedMinMinus1PlusA) triedMaybeN)

-> { min : Nat (N min (Is minToTriedMin To triedMin) x) }

-> { less : Nat (In min triedMinMinus1PlusA maybeN) -> result

, equalOrGreater : Nat (ValueMin triedMin) -> result

}

-> Nat (In min max maybeN)

-> result

Is the Nat (ValueMin ...)

equalOrGreater than a Nat or
less?

factorial : MinNat min -> MinNat Nat1
factorial =
    MNat.lowerMin nat0
        >> MinNat.isAtLeast nat1
            { min = nat0 }
            { less = \_ -> nat1 |> Nat.toMin
            , equalOrGreater =
                \atLeast1 ->
                    atLeast1
                        |> Nat.mul
                            (factorial
                                (atLeast1 |> MinNat.subN nat1)
                            )
            }

isAtMost :

Nat (In atMostMin atLeastAtMostMin atMostMaybeN)

-> { min : Nat (N min (Is minToAtMostMin To atMostMin) x) }

-> { equalOrLess : Nat (In min atLeastAtMostMin maybeN) -> result

, greater : Nat (ValueMin (Nat1Plus atMostMin)) -> result

}

-> Nat (In min max maybeN)

-> result

Is the Nat (ValueMin ...)

equalOrLess than a Nat or
greater?

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

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

modify

subN :

Nat (N subbed (Is differenceMin To min) x)

-> Nat (In min max maybeN)

-> Nat (ValueIn differenceMin max)

Subtract an exact Nat (N ...).

atLeast7 |> MinNat.subN nat2
--> is of type Nat (ValueMin Nat5)

add :

Nat (In minAdded maxAdded addedMaybeN)

-> Nat (N minAdded (Is min To sumMin) x)

-> Nat (In min max maybeN)

-> Nat (ValueMin sumMin)

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

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

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

sub :

Nat (In minSubbed maxSubbed subbedMaybeN)

-> Nat (N maxSubbed (Is differenceMin To min) x)

-> Nat (In min max maybeN)

-> Nat (ValueIn differenceMin max)

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.

addN :

Nat (N added (Is min To sumMin) x)

-> Nat (In min max maybeN)

-> Nat (ValueMin sumMin)

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

atLeast70 |> InNat.addN nat7
--> is of type Nat (ValueMin Nat77)

lue-bird/elm-bounded-nat/5.0.1

MinNat

compare

modify

Modules