A natural number within a minimum & maximum.
Cap the Nat (In ...) to at most a number.
nat5 |> NNat.toIn
|> InNat.atMost (nat10 |> NNat.toIn) { min = nat5 }
--> InNat 5
nat15 |> NNat.toIn |> InNat.lowerMin (nat5 |> NNat.toIn)
|> InNat.atMost (nat10 |> NNat.toIn) { min = nat5 }
--> Nat 10min ensures that that number is at least the minimum.
The maximum can also be Infinity.
nat5 |> NNat.dropMax
|> InNat.atMost (nat10 |> NNat.toIn) { min = nat5 }
--> Nat 5Compare 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 |> NNat.toIn)
>> 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) } -> ExperienceCompared to a range first to last, is the Nat (In ...)
inRange
greater than the last or
less than the first?
justIfBetween3And10 =
InNat.lowerMin (nat0 |> NNat.toIn)
>> InNat.isInRange { first = nat3, last = nat10 }
{ min = nat0 }
{ less = \_ -> Nothing
, greater = \_ -> Nothing
, inRange = Just
}
justIfBetween3And10 (nat9 |> NNat.toIn)
--> Just (Nat 9)
justIfBetween3And10 (nat123 |> NNat.toIn)
--> NothingIs the Nat (In ...)
equalOrGreater than a Nat or
less?
vote : { age : Nat (In (Nat18Plus orOlder) max) } -> Vote
tryToVote =
InNat.lowerMin (nat0 |> NNat.toIn)
>> 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 |> NNat.toIn)
>> 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))Use [MinNat.addN] if the maximum value is Infinity.
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
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))Divide (//) by a Nat (In ...).
/ 0 is impossible
x / d is at most x
nat7 |> NNat.toIn
|> InNat.div (nat3 |> NNat.dropMax)
--> Nat 2 of type Nat (In Nat0 (Nat7Plus a))The remainder after division.
% 0 is impossiblex % d is at most xNNat.toIn nat7 |> InNat.remainderBy (nat3 |> NNat.dropMax)
--> Nat 1 of type Nat (In Nat0 (Nat7Plus a))Subtract a Nat (In ..) without
nat6 |> NNat.dropMax
|> 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 (Min Nat5)
atLeast2 |> MinNat.addLossy atLeast5 --> is of type Nat (Min Nat2)
Either of the 2 added Nats can bhave a maximum of Infinity.
If you know the minimum and maximum added value at hand, use add.
Multiply by a Nat (In ...) >= 1.
we know that if a >= 1, x * a >= x.
nat5 |> NNat.toIn |> MinNat.mul (nat2 |> NNat.toIn)
--> Nat 10 of type Nat (Min Nat5)
nat2 |> NNat.toIn |> MinNat.mul (nat5 |> NNat.toIn)
--> Nat 10 of type Nat (Min Nat2)The maximum value of both factors can be Infinity.
The Nat (Min ...) ^ a Nat (Min ...).
We know that if a >= 1 → x ^ a >= x
five |> MinNat.toPower two
--> Nat 25 of type Nat (Min Nat5)
two |> MinNat.toPower five
--> Nat 25 of type Nat (Min Nat2)
two = nat2 |> NNat.toIn
five = nat5 |> NNat.toInThe maximum of both the base and the power can be Infinity.
Set the minimum lower.
[ NNat.toIn nat3, NNat.toIn nat4 ]Elm complains:
But all the previous elements in the list are:
Nat (In Nat3 ...)
[ NNat.toIn nat3
, NNat.toIn nat4 |> InNat.lowerMin (nat3 |> NNat.toIn)
]Make it fit into functions with higher maximum.
You should design type annotations as general as possible.
onlyAtMost18 : Nat (In min Nat18)
onlyAtMost18 between3And8 --fineBut 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 (Min min).
in4To10 |> NNat.dropMax
--> is of type Nat (Min Nat4)There is only 1 situation you should use this.
To make 2 Nats the same type.
[ atLeast1, in1To10 ]Elm complains:
But all the previous elements in the list are:
Nat (In Nat1 Infinity)
[ atLeast1
, in1To10 |> InNat.dropMax
]Generate a random Nat (In ...) in a range.
Nat (In ...)s from a first to a last value.
from3To10 =
InNat.range (nat3 |> NNat.toIn) (nat10 |> NNat.toIn)The resulting List is never empty.
Notice that the maximum value of the last can be Infinity.
InNat.range (nat3 |> NNat.toIn) (nat10 |> NNat.dropMax)
--> List (Nat (In Nat3 Infinity))
--> alias to List (Nat (Min Nat3))
If the
Nat (In ...)is less than a number, return that number instead.Notice that this also works, if the
maxisInfinity.