MinNat

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

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

nat3 |> NNat.toIn
    |> InNat.mul (nat3 |> NNat.toIn)
--> Nat (Min Nat3)

The maximum isn't fixed

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

compare

is :

Nat (In (Nat1Plus triedMinus1) (Nat1Plus triedMinus1PlusA))

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

-> { equal : () -> result

, less : Nat (In min triedMinus1PlusA) -> result

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

}

-> Nat (In min max)

-> result

Compare the Nat (Min ...) 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 |> NNat.toIn)
        >> MinNat.is (nat18 |> NNat.toIn)
            { 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

isAtLeast :

Nat (In triedMin (Nat1Plus triedMinMinus1PlusA))

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

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

, equalOrGreater : Nat (Min triedMin) -> result

}

-> Nat (In min max)

-> result

Is the Nat (Min ...)

equalOrGreater than a Nat or
less?

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

isAtMost :

Nat (In atMostMin atMostMinPlusA)

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

-> { equalOrLess : Nat (In min atMostMinPlusA) -> result

, greater : Nat (Min atMostMin) -> result

}

-> Nat (In min max)

-> result

Is the Nat (Min ...)

equalOrLess than a Nat or
greater?

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

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

modify

subN :

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

-> Nat (In min max)

-> Nat (In differenceMin max)

Subtract an exact Nat (N ...).

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

add :

Nat (In addedMin max)

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

-> Nat (In min max)

-> Nat (Min sumMin)

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

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

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

sub :

Nat (In minSubtracted maxSubtracted)

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

-> Nat (In min max)

-> Nat (In differenceMin max)

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

atLeast6 |> InNat.subLossyMax 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)

-> Nat (Min sumMin)

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

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

For every other operation, use InNat.

indique/elm-bounded-nat/9.0.0

MinNat

compare

modify

Modules