TypeLevel.Nat.Proofs

Some proofs on type-level Peano numbers.

Documentation

plusAssoc :: The Nat x -> p y -> q z -> ((x + y) + z) :~: (x + (y + z))

Addition is associative.

plusZeroNeutral :: The Nat n -> (n + Z) :~: n

Zero is the identity of addition.

plusSuccDistrib :: The Nat n -> proxy m -> (n + S m) :~: S (n + m)

Successor distributes over addition