Modulenatural-arithmetic-0.2.4.0Haskell2010

Arithmetic.Plus

valuezeroL :: m :=: (0 + m)

Zero plus any number is equal to the original number.

valuezeroR :: m :=: (m + 0)

Any number plus zero is equal to the original number.

valuecommutative :: (a + b) :=: (b + a)

Addition is commutative.

valuecommutative# :: (# #) -> (a + b) :=:# (b + a)

valueassociative :: ((a + b) + c) :=: (a + (b + c))

Addition is associative.