NNat

modify

Nat (N n (Is a To nPlusA) (Is b To nPlusB))

-> Nat

(Nat1Plus n)

(Is a To (Nat1Plus nPlusA))

(Is b To (Nat1Plus nPlusB))

)

The Nat (N ...) plus 1.

Keep in mind that if you want add any number, rather go for Nat (In ...) or Nat (Min ...).

Nat

(Nat1Plus nMinus1)

(Is a To (Nat1Plus nMinus1PlusA))

(Is b To (Nat1Plus nMinus1PlusB))

)

-> Nat (N nMinus1 (Is a To nMinus1PlusA) (Is b To nMinus1PlusB))

The Nat (N ...) minus 1.

Keep in mind that if you want subtract any number, rather go for Nat (In ...) or Nat (Min ...).

toMin : Nat (N n x y) -> Nat (Min n)

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
]

toIn : Nat (N n (Is a To nPlusA) x) -> Nat (In n nPlusA)

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

The minimum is n, the maximum >= n.