Safe Haskell	None
Language	Haskell2010

Arithmetic.Plus

Synopsis

zeroL :: forall (m :: Nat). m :=: (0 + m)
zeroR :: forall (m :: Nat). m :=: (m + 0)
commutative :: forall (a :: Natural) (b :: Natural). (a + b) :=: (b + a)
commutative# :: forall (a :: Natural) (b :: Natural). (# #) -> (a + b) :=:# (b + a)
associative :: forall (a :: Natural) (b :: Natural) (c :: Natural). ((a + b) + c) :=: (a + (b + c))

Documentation

zeroL :: forall (m :: Nat). m :=: (0 + m) Source #

Zero plus any number is equal to the original number.

zeroR :: forall (m :: Nat). m :=: (m + 0) Source #

Any number plus zero is equal to the original number.

commutative :: forall (a :: Natural) (b :: Natural). (a + b) :=: (b + a) Source #

Addition is commutative.

commutative# :: forall (a :: Natural) (b :: Natural). (# #) -> (a + b) :=:# (b + a) Source #

associative :: forall (a :: Natural) (b :: Natural) (c :: Natural). ((a + b) + c) :=: (a + (b + c)) Source #

Addition is associative.