NNat

Representing natural numbers (>=0).

This module lets you represent exact values in the NNat type.

This means, packages like elm-n-array can use a NNat to promise:

fromRepeating : NNat n -> element -> NArray n element

→ repeating an element n times gives a Array with n elements!

The other use is to describe a difference between two values.

interval :
    { first : NNat (N first Is (Difference range To last))
    , last : NNat (N last Is lastDifference)
    }
-> Interval

→ because range is 0 or positive, last must also be at least as high as first.

See the readme for more information.

type alias NNat n =

NNat n

A natural number (<= 0), where you know the exact value.

NNat.n3 is of type

NNat (N N3Nat Is (Difference a To (N3NatPlus a)))

This means, its exact value can be described as

N3Nat
the Diffence of some a to a plus 3.

transform

toInt : NNat n -> Int

Convert a NNat to an Int.

NNat.n4 |> NNat.toInt
--> 4

add

add1 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat1Plus n) Is (Difference a To (Nat1Plus nPlusA)))

The NNat plus 1.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add10 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat10Plus n) Is (Difference a To (Nat10Plus nPlusA)))

The NNat plus 10.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add11 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat11Plus n) Is (Difference a To (Nat11Plus nPlusA)))

The NNat plus 11.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add12 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat12Plus n) Is (Difference a To (Nat12Plus nPlusA)))

The NNat plus 12.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add13 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat13Plus n) Is (Difference a To (Nat13Plus nPlusA)))

The NNat plus 13.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add14 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat14Plus n) Is (Difference a To (Nat14Plus nPlusA)))

The NNat plus 14.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add15 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat15Plus n) Is (Difference a To (Nat15Plus nPlusA)))

The NNat plus 15.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add16 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat16Plus n) Is (Difference a To (Nat16Plus nPlusA)))

The NNat plus 16.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add2 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat2Plus n) Is (Difference a To (Nat2Plus nPlusA)))

The NNat plus 2.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add3 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat3Plus n) Is (Difference a To (Nat3Plus nPlusA)))

The NNat plus 3.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add4 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat4Plus n) Is (Difference a To (Nat4Plus nPlusA)))

The NNat plus 4.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add5 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat5Plus n) Is (Difference a To (Nat5Plus nPlusA)))

The NNat plus 5.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add6 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat6Plus n) Is (Difference a To (Nat6Plus nPlusA)))

The NNat plus 6.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add7 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat7Plus n) Is (Difference a To (Nat7Plus nPlusA)))

The NNat plus 7.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add8 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat8Plus n) Is (Difference a To (Nat8Plus nPlusA)))

The NNat plus 8.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

add9 :

NNat (N n Is (Difference a To nPlusA))

-> NNat (N (Nat9Plus n) Is (Difference a To (Nat9Plus nPlusA)))

The NNat plus 9.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

at least

sub1 :

NNat

(Nat1Plus nMinus1)

(Difference a To (Nat1Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 1.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub10 :

NNat

(Nat10Plus nMinus1)

(Difference a To (Nat10Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 10.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub11 :

NNat

(Nat11Plus nMinus1)

(Difference a To (Nat11Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 11.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub12 :

NNat

(Nat12Plus nMinus1)

(Difference a To (Nat12Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 12.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub13 :

NNat

(Nat13Plus nMinus1)

(Difference a To (Nat13Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 13.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub14 :

NNat

(Nat14Plus nMinus1)

(Difference a To (Nat14Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 14.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub15 :

NNat

(Nat15Plus nMinus1)

(Difference a To (Nat15Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 15.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub16 :

NNat

(Nat16Plus nMinus1)

(Difference a To (Nat16Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 16.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub2 :

NNat

(Nat2Plus nMinus1)

(Difference a To (Nat2Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 2.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub3 :

NNat

(Nat3Plus nMinus1)

(Difference a To (Nat3Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 3.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub4 :

NNat

(Nat4Plus nMinus1)

(Difference a To (Nat4Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 4.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub5 :

NNat

(Nat5Plus nMinus1)

(Difference a To (Nat5Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 5.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub6 :

NNat

(Nat6Plus nMinus1)

(Difference a To (Nat6Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 6.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub7 :

NNat

(Nat7Plus nMinus1)

(Difference a To (Nat7Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 7.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub8 :

NNat

(Nat8Plus nMinus1)

(Difference a To (Nat8Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 8.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

sub9 :

NNat

(Nat9Plus nMinus1)

(Difference a To (Nat9Plus nPlusAMinus1))

)

-> NNat (N nMinus1 Is (Difference a To nPlusAMinus1))

The NNat minus 9.

Keep in mind, that if you want do calculations, rather go for nat-in-range.

indique/elm-n-nat/4.0.0

NNat

transform

add

at least

Modules