type-indexed-queues-0.1.0.0: Queues with verified and unverified versions.
TypeLevel.Nat.Proofs
Description
Some proofs on type-level Peano numbers.
Synopsis
plusAssoc :: The Nat x -> p y -> q z -> ((x + y) + z) :~: (x + (y + z)) Source #
Addition is associative.
plusZeroNeutral :: The Nat n -> (n + Z) :~: n Source #
Zero is the identity of addition.
plusSuccDistrib :: The Nat n -> proxy m -> (n + S m) :~: S (n + m) Source #
Successor distributes over addition