N.Type

See the readme for more information.

type N n is difference

You might want a function, where one N-X-Nat should be at least as big as another one.

unsafeInterval : NaturalNumber first -> NaturalNumber last -> Interval

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 (N first Is (Difference interval To last))
    -> NNat (N last Is difference)
    -> Interval

type Is

No special meaning.

N n Is difference

type Difference a to b

b - a.

Difference a To (Nat1Plus a)

would describe a difference of 1.

type To

No special meaning.

Difference a To b

Modules