Type.Family.Nat

Type-level natural numbers, along with frequently used type families over them.

Documentation

data N

Constructors

Z

S N

Instances

Eq N

Ord N

Show N

TestEquality N Nat

Read1 N Nat

Read1 N Fin

Show1 N Nat

Show1 N Fin

Ord1 N Nat

Ord1 N Fin

Eq1 N Nat

Eq1 N Fin

Known N Nat Z

Z_ is the canonical construction of a Nat Z.

Known N Nat n => Known N Nat (S n)

If n is a canonical construction of Nat n, S_ n is the canonical construction of Nat (S n).

(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n)

A Fin n is a Witness that n >= 1.

That is, Pred n is well defined.

Witness ØC (Known N Nat n) (Nat n)

A Nat n is a Witness that there is a canonical construction for Nat n.

Witness ØC (Known N Nat n) (VT k n f a)

type (==) N x y = NatEq x y

type KnownC N Nat Z = ØC

type KnownC N Nat (S n) = Known N Nat n

type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n)

type WitnessC ØC (Known N Nat n) (Nat n) = ØC

type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC

fromInt :: Int -> Maybe N

type family IsZero x :: Bool

Equations

IsZero Z = True

IsZero (S x) = False

zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)

zNotS :: (Z ~ S x) :- Fail

type family NatEq x y :: Bool

Equations

NatEq Z Z = True

NatEq Z (S y) = False

NatEq (S x) Z = False

NatEq (S x) (S y) = NatEq x y

type family Iota x :: [N]

Equations

Iota Z = Ø

Iota (S x) = x :< Iota x

iotaCong :: (x ~ y) :- (Iota x ~ Iota y)

type family Pred x :: N

Equations

Pred (S n) = n

predCong :: (x ~ y) :- (Pred x ~ Pred y)

type family x + y :: N infixr 6

Equations

Z + y = y

(S x) + y = S (x + y)

addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))

type family x * y :: N infixr 7

Equations

Z * y = Z

(S x) * y = (x * y) + y

mulCong :: (w ~ y, x ~ z) :- ((w * x) ~ (y * z))

type family x ^ y :: N infixl 8

Equations

x ^ Z = S Z

x ^ (S y) = (x ^ y) * x

expCong :: (w ~ y, x ~ z) :- ((w ^ x) ~ (y ^ z))

type family Len as :: N

Equations

Len Ø = Z

Len (a :< as) = S (Len as)

lenCong :: (as ~ bs) :- (Len as ~ Len bs)

type family Ix x as :: k

Equations

Ix Z (a :< as) = a

Ix (S x) (a :< as) = Ix x as

ixCong :: (x ~ y, as ~ bs) :- (Ix x as ~ Ix y bs)

type N0 = Z

Convenient aliases for low-value Peano numbers.

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9