
  0 | module Data.Alg
  1 | 
  2 | import Data.Coproduct
  3 | import Data.Product
  4 | 
  5 | %default total
  6 | 
  7 | public export
  8 | distributePlus : a * (b + c) -> a * b + a * c
  9 | distributePlus (fst && (+> x)) = +> (fst && x)
 10 | distributePlus (fst && (<+ x)) = <+ (fst && x)
 11 | 
 12 | ||| distributive property of products over coproducts
 13 | public export
 14 | distributive : (p * p') * (s + s') -> (p * s) + (p' * s')
 15 | distributive ((fst && snd) && (<+ x)) = <+ (fst && x)
 16 | distributive ((fst && snd) && (+> x)) = +> (snd && x)
 17 | 
 18 | ||| distributive property of products over coproducts
 19 | public export
 20 | distributive' :  (p + q) * (a * b) -> (p * a) + (q * b)
 21 | distributive' ((<+ x) && a && b) = <+ (x && a)
 22 | distributive' ((+> x) && a && b) = +> (x && b)
 23 | 
 24 | ||| x + x is 2 * x
 25 | multiply : a + a -> Bool * a
 26 | multiply = choice (True &&) (False &&)
 27 |