module Data.Semiring.Properties (
module Data.Semiring, module Data.Semiring.Properties
) where
import Data.Semiring
plus'comm :: Semiring s => s -> s -> Bool
plus'comm a b = a .+. b == b .+. a
left'zero :: Semiring s => s -> Bool
left'zero a = zero .+. a == a
add'assoc :: Semiring s => s -> s -> s -> Bool
add'assoc a b c = (a .+. b) .+. c == a .+. (b .+. c)
left'one :: Semiring s => s -> Bool
left'one a = one .*. a == a
right'one :: Semiring s => s -> Bool
right'one a = a .*. one == a
mul'assoc :: Semiring s => s -> s -> s -> Bool
mul'assoc a b c = (a .*. b) .*. c == a .*. (b .*. c)
left'distr :: Semiring s => s -> s -> s -> Bool
left'distr a b c = a .*. (b .+. c) == (a .*. b) .+. (a .*. c)
right'distr :: Semiring s => s -> s -> s -> Bool
right'distr a b c = (a .+. b) .*. c == (a .*. c) .+. (b .*. c)
left'ann :: Semiring s => s -> Bool
left'ann a = zero .*. a == zero
right'ann :: Semiring s => s -> Bool
right'ann a = a .*. zero == zero