indique/elm-bounded-nat/2.0.0

NOTE: the latest version is 13.0.0

Nat.Min

A Nat which is at least some minimum.

add information

abs : Int -> Nat (Min Nat0)

The absolute value of an Int, which is at least Nat0.

Nat.Min.abs 16 --> Nat.Min 16


Nat.Min.abs -4 --> Nat.Min 4

Really only use this if you want the absolute value.

badLength list =
    List.length >> Nat.Min.abs


goodLength =
    List.foldl
        (\_ -> Nat.Min.addN nat1 >> Nat.Min.lowerMin nat0)
        (Nat.Min.n nat0)

If something like this isn't possible, use Nat.Min.intAtLeastnat0!

clamp

Nat (N max Is (Difference a To maxPlusA))
-> { min : Nat (N min Is (Difference range To max)) }
-> Nat (Min min)
-> Nat (In min maxPlusA)

Cap the Nat (Min ...) to at most a upper limit.

atMost5 : Nat (Min min) -> Nat (Min Nat5)
atMost5 =
    Nat.Min.lowerMin nat0
        >> Nat.Min.atMost (nat5 |> Nat.Min.n) { min = nat0 }


atMost5 (nat12 |> Nat.Min.n) --> Nat 5
atMost5 (nat3 |> Nat.Min.n) --> Nat 3
intAtLeast : Nat (N n Is difference) -> Int -> Nat (Min n)

A Nat.Min from an Int; if the Int < minimum, minimum is returned.

9 |> Nat.Min.intAtLeast nat3 --> Nat.Min 9


0 |> Nat.Min.intAtLeast nat3 --> Nat.Min 3

You can also use this if you know an Int must be at least minimum.

But avoid it if you can do better, like

goodLength =
    List.foldl
        (\_ -> Nat.Min.addN nat1 >> Nat.Min.lowerMin nat0)
        (Nat.Min.n nat0)

If you want to handle the case < minimum yourself, use Nat.Min.isIntAtLeast.

atLeast : Nat (Only newMin) -> Nat (Min min) -> Nat (Min newMin)

If the Nat (Min ...) is lower than a lower limit, return the lower limit instead.

atLeast5 : Nat (Min min) -> Nat (Min Nat5)
atLeast5 =
    Nat.Min.atLeast (nat5 |> Nat.Min.n)


atLeast5 (nat3 |> Nat.Min.n) --> Nat 5
atLeast5 (nat12 |> Nat.Min.n) --> Nat 12

compare

isIntAtLeast : Nat (N min Is difference) -> Int -> Maybe (Nat (Min n))

If the Int >= a minimum, Just the Nat.Min, else Nothing.

4 |> Nat.Min.isIntAtLeast nat5 --> Nothing


1234 |> Nat.Min.isIntAtLeast nat5 --> Just (NatIn 1234)
is :
Nat
(N
(Nat1Plus triedMinus1)
(Difference (Nat1Plus aMinus1) To (Nat1Plus triedMinus1PlusA))
)
-> { min : Nat (N min Is (Difference lessRange To triedMinus1)) }
-> { equal : () -> result
, less : Nat (In min triedMinus1PlusA) -> result
, greater : Nat (Min (Nat2Plus triedMinus1)) -> result
}
-> Nat (Min min)
-> result

Compared to an exact Nat.

Nat
(N
triedMin
(Difference a To (Nat1Plus triedMinMinus1PlusA))
)
-> { min :
Nat (N min Is (Difference (Nat1Plus lessRange) To triedMin))
}
-> { less : Nat (In min triedMinMinus1PlusA) -> result
, equalOrGreater : Nat (Min triedMin) -> result
}
-> Nat (Min min)
-> result

Is the Nat (Min ...)

  • equalOrGreater than a Nat or

  • less?

factorialHelp : Nat.Min min -> Nat.Min Nat1
factorialHelp =
    Nat.Min.lowerMin nat0
        >> Nat.Min.isAtLeast nat1
            { min = nat0 }
            { less = \_ -> Nat.Min.n nat1
            , equalOrGreater =
                \oneOrGreater ->
                    oneOrGreater
                        |> Nat.Min.mul
                            (factorialHelp
                                (oneOrGreater |> Nat.Min.subN nat1)
                            )
            }
Nat (N atMostMin Is (Difference a To atMostMinPlusA))
-> { min : Nat (N min Is (Difference minToAtMostMin To atMostMin))
}
-> { equalOrLess : Nat (In min atMostMinPlusA) -> result
, greater : Nat (Min atMostMin) -> result
}
-> Nat (Min min)
-> result

Is the Nat.Min

  • equalOrLess than a Nat or

  • greater?

theGreater : Nat (Min min) -> Nat (Min min) -> Nat (Min min)

The greater of 2 Nat.Mins. Works just like Basics.max.

Nat.Min.theGreater
    (nat3 |> Nat.Min.n)
    (nat4 |> Nat.Min.n |> Nat.Min.lowerMin nat3)
--> Nat.Min 4
theSmaller : Nat (Min min) -> Nat (Min min) -> Nat (Min min)

The smaller of 2 Nat.Mins. Works just like Basics.min.

Nat.Min.theSmaller
    (nat3 |> Nat.Min.n)
    (nat4 |> Nat.Min.n |> Nat.Min.lowerMin nat3)
--> Nat.Min 3

drop information

n : Nat (N n Is difference) -> Nat (Min n)

Convert an exact Nat n to a Nat.Min n (n + a).

Nat.Min.n nat4
--> is of type Nat (Min Nat4)
Nat (N lowerMin Is (Difference howMuchLower To min))
-> Nat (Min min)
-> Nat (Min lowerMin)

Set the minimum lower.

modify

Nat (N n Is (Difference min To minPlusN))
-> Nat (Min min)
-> Nat (Min minPlusN)

Add an exact Nat.

(nat5 |> Nat.Min.n)
    |> Nat.Min.addN nat2
--> Nat.Min 7
Nat (N n Is (Difference minMinusN To min))
-> Nat (Min min)
-> Nat (Min minMinusN)

Subtract an exact Nat.

(nat7 |> Nat.Min.n)
    |> Nat.Min.subN nat2
--> Nat.Min 5
add :
Nat (Min addedMin)
-> Nat (N addedMin Is (Difference min To sumMin))
-> Nat (Min min)
-> Nat (Min sumMin)

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

(nat5 |> Nat.Min.n)
    |> Nat.Min.add atLeast2 nat2
Nat (In subtractedMin subtractedMax)
-> Nat (N subtractedMax Is (Difference differenceMin To min))
-> Nat (Min min)
-> Nat (Min differenceMin)

Subtract a InNat. The second argument is the maximum if the subtracted InNat.

(nat5 |> Nat.Min.n)
    |> Nat.Min.subIn inNat0To5 itsMaximum
mul :
Nat (Min (Nat1Plus multipliedMinMinus1))
-> Nat (Min min)
-> Nat (Min min)

Multiply by a Nat.Min >= 1. We can't compute the highest possiblenew minimum, we only know that if a >= 1 → x * a >= x

five |> Nat.Min.mul two
--> Nat.Min 10, but the type is Nat.Min Nat5


two |> Nat.Min.mul five
--> Nat.Min 10, but the type is Nat.Min Nat2


two = nat2 |> Nat.Min.n


five = nat5 |> Nat.Min.n
div : Nat (Min (Nat1Plus minMinus1)) -> Nat (Min min) -> Nat (Min Nat0)

Divide (//) by a Nat.Min. div 0 is impossible.

Nat.Min.n nat7 |> Nat.Min.div (Nat.Min.n nat3)
--> Nat.Min 2 of type Nat.Min Nat0
remainderBy : Nat (Min (Nat1Plus dMinMinus1)) -> Nat (Min min) -> Nat (Min Nat0)

The remainder after division. remainderBy 0 is impossible.

Nat.Min.n nat7 |> Nat.Min.remainderBy (Nat.Min.n nat3)
--> Nat.Min Nat0
toPower : Nat (Min (Nat1Plus minMinus1)) -> Nat (Min min) -> Nat (Min min)

The Nat.Min ^ a Nat.Min. We can't compute the highest possible new minimum, we only know that if a >= 1 → x ^ a >= x

five |> Nat.Min.toPower two
--> Nat.Min 25, but the type is Nat.Min Nat5


two |> Nat.Min.mul five
--> Nat.Min 25, but the type is Nat.Min Nat2


two = nat2 |> Nat.Min.n


five = nat5 |> Nat.Min.n

extra

Nat (In firstMin lastMin)
-> Nat (Min lastMin)
-> List (Nat (Min firstMin))

Nat.Mins from a first InNat to a last Nat.Min.