Short for add ( nat1, nat1 ). See add on how to use it properly.

Short for sub ( nat1, nat1 ). See sub on how to use it properly.

The Nat (N ...) plus another Nat (N ...). Give the added value twice as a tuple.

nat6 |> NNat.add ( nat5, nat5 )
--> Nat 11 of type
--> Nat
-->     (N Nat11
-->         (Is a To Nat11Plus a)
-->         (Is b To Nat11Plus b)
-->     )

This is only rarely useful, as you shouldn't

inRangeXAndXPlus10 x =
    -- won't work
    isInRange x (x |> NNat.add ( nat10, nat10 ))


isAtLeast10GreaterThan x =
    -- the only use case
    isAtLeast (x |> NNat.add ( nat10, nat10 ))

(examples don't compile, just for demonstration)

Using a Nat (In ...) is often the better choice.

The Nat (N ...) plus another Nat (N ...). Give the added value twice as a tuple.

nat6 |> NNat.sub ( nat5, nat5 )
--> Nat 1 of type
--> Nat
-->     (N Nat1
-->         (Is a To Nat1Plus a)
-->         (Is b To Nat1Plus b)
-->     )

This is only rarely useful, as you shouldn't

inRangeXMinus10ToX x =
    -- won't work
    isInRange (x |> NNat.sub ( nat10, nat10 )) x


isAtLeast10LessThan x =
    -- the only use case
    isAtLeast (x |> NNat.sub ( nat10, nat10 ))

(examples don't compile, just for demonstration)

Using a Nat (In ...) is often the better choice.

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

nat4 |> NNat.toMin
--> is of type Nat (Min Nat4)

There is only 1 situation you should use this.

To make 2 Nats of the same type.

[ atLeast1, NNat.toIn nat1 ]

Elm complains:

But all the previous elements in the list are: Nat (In Nat1 Infinity)

[ atLeast1
, NNat.toMin nat4
]

A Nat (In ...) from an exact Nat (N n ...).

The minimum is n, the maximum >= n.