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) -> Charyou should use InNat operations.
If the maximum isn't known, use the operations in MinNat.
If the Nat (In ...) is less than a number, return that number instead.
nat5 |> InNat.atLeast nat10
--> Nat 10
nat15 |> InNat.atLeast nat10
--> Nat 15Compare 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) } -> ExperienceCompared 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
--> NothingIs 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 })
}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
}Add a fixed Nat (N ...) value.
between70And100
|> InNat.addN nat7
--> is of type Nat (In Nat77 (Nat107Plus a))Subtract a fixed Nat value.
between7And10
|> InNat.subN nat7
--> is of type Nat (ValueIn Nat0 (Nat3Plus a))Use MinNat.subN if the maximum value is not known.
Add a Nat (In ...).
between3And10
|> InNat.add between1And12 nat1 nat12
--> is of type Nat (In Nat4 (Nat22Plus a))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))
Cap the
Nat (In ...)to at most a number.minensures that that number is at least the minimum.