Data.Alg

Definitions

distributePlus : a * (b + c) -> (a * b) + (a * c)

Totality: total
Visibility: public export

distributive : (p * p') * (s + s') -> (p * s) + (p' * s')

  distributive property of products over coproducts

Totality: total
Visibility: public export

distributive' : (p + q) * (a * b) -> (p * a) + (q * b)

  distributive property of products over coproducts

Totality: total
Visibility: public export