InNat

Operations when you know the maximum of the Nat (In minimum maximum maybeN).

For example for the argument in

toHexChar : Nat (In min Nat15 maybeN) -> Char

you should use InNat operations.

If the maximum isn't known, use the operations in MinNat.

add information

clamp

atMost :

Nat (In minNewMax atLeastNewMax newMaxMaybeN)

-> { min : Nat (N min (Is minToMinNewMax To minNewMax) x) }

-> Nat (In min max maybeN)

-> Nat (ValueIn min atLeastNewMax)

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

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


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

min ensures that that number is at least the minimum.

atLeast :

Nat (In newMin max lowerMaybeN)

-> Nat (In min max maybeN)

-> Nat (ValueIn newMin max)

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

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


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

compare

is :

Nat

tried

(Is triedToMax To max)

(Is a To (Nat1Plus atLeastTriedMinus1))

)

-> { min : Nat (N min (Is minToTried To tried) x) }

-> { equal : () -> result

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

, greater : Nat (In (Nat2Plus triedMinus1) max maybeN) -> result

}

-> Nat (In min max maybeN)

-> result

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

isInRange :

{ first :

Nat

first

(Is firstToLast To last)

(Is firstA To (Nat1Plus atLeastFirstMinus1))

)

, last :

Nat (N last (Is lastToMax To max) (Is lastA To atLeastLast))

}

-> { min : Nat (N min (Is minToFirst To first) x) }

-> { inRange : Nat (In first atLeastLast maybeN) -> result

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

, greater : Nat (In (Nat1Plus last) max maybeN) -> result

}

-> Nat (In min max maybeN)

-> result

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

inRange
greater than the last or
less than the first?

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

justIfBetween3And10 nat9
--> Just (Nat 9)

justIfBetween3And10 nat123
--> Nothing

isAtLeast :

Nat

tried

(Is a To (Nat1Plus atLeastTriedMinus1))

(Is atLeastRange To max)

)

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

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

, equalOrGreater : Nat (In tried max maybeN) -> result

}

-> Nat (In min max maybeN)

-> result

Is the Nat (In ...)

equalOrGreater than a Nat or
less?

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

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

isAtMost :

Nat

tried

(Is a To atLeastTried)

(Is (Nat1Plus greaterRange) To max)

)

-> { min : Nat (N min (Is minToTried To tried) x) }

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

, greater : Nat (In (Nat1Plus tried) max maybeN) -> result

}

-> Nat (In min max maybeN)

-> result

Is the Nat (In ...)

equalOrLess than a Nat or
greater?

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

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

modify

addN :

Nat (N added (Is min To sumMin) (Is max To sumMax))

-> Nat (In min max maybeN)

-> Nat (ValueIn sumMin sumMax)

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

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

subN :

Nat (N sub (Is differenceMin To min) (Is differenceMax To max))

-> Nat (In min max maybeN)

-> Nat (ValueIn differenceMin differenceMax)

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 :

Nat (In addedMin addedMax addedMaybeMax)

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

-> Nat (N addedMax (Is max To sumMax) y)

-> Nat (In min max maybeN)

-> Nat (ValueIn sumMin sumMax)

Add a Nat (In ...).

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

sub :

Nat (In minSubbed maxSubbed subbedMaybeN)

-> Nat (N minSubbed (Is differenceMax To max) x)

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

-> Nat (In min max maybeN)

-> Nat (ValueIn differenceMin differenceMax)

Subtract a Nat (In ...).

The 2 following arguments are

the minimum subtracted value
the maximum subtracted value
in6To12 |> InNat.sub in1And5 nat1 nat5 --> is of type Nat (In Nat1 (Nat5Plus a))

lue-bird/elm-bounded-nat/4.0.0

InNat

add information

clamp

compare

modify

Modules