module Test.Operation.Distributive where

import Test.Util


-- | \( \forall a, b, c: (a \# b) \% c \equiv (a \% c) \# (b \% c) \)
--
distributive :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
distributive = distributive_on (==)

-- | \( \forall a, b, c: c \% (a \# b) \equiv (c \% a) \# (c \% b) \)
--
distributive' :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
distributive' = distributive_on' (==)

distributive_on :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
distributive_on (~~) (#) (%) a b c = ((a # b) % c) ~~ ((a % c) # (b % c))

distributive_on' :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
distributive_on' (~~) (#) (%) a b c = (c % (a # b)) ~~ ((c % a) # (c % b))