indique/elm-n-type/1.0.0

elm-n-type

We go on where we left off in elm-n-nat-type.

You might also want a function, where one NaturalNat should be at least as big as another one.

unsafeInterval : NaturalNumber first -> NaturalNumber maybeMoreThanFirst -> Interval

import N.Nat.Type exposing (..)
import N.Type exposing (..)


--we don't expose the constructor
type NNat n =
    NNat Int

zero : NNat (N N0Nat Is (Diffence a To a))
zero =
    NNat one

add1 :
    NNat (N n Is (Difference a To nPlusA))
    -> NNat (N (N1NatPlus n) Is (Difference a To (N1NatPlus nPlusA))
add1 (NNat int) =
    NNat (int + 1)

We can now see if the difference between two values is a certain value!

We want to promise that

last == first + the interval length

which means

first == last - the interval length

→ N first Is (Difference intervalLength To last) is our final type 🔥!

safeInterval :
    NNat first (Plus maybeMore Is last)
    -> NNat last describesADelta
    -> Interval

This package together with elm-n-nat-type is the foundation of elm-n-nat, elm-nat-within, elm-n-array.

Take a closer look at those packages to see N.Type in action!