module BoolRing where
open import Function
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Structures
open import BoolTactic
boolRing : Ring
boolRing =
record {
C = Bool;
`0 = false;
`1 = true;
_+_ = _xor_;
_*_ = _∧_;
-_ = id;
isRing =
record {
+-isAbelianGroup =
record { isGroup =
record { isMonoid = record { left-id = auto _;
right-id = auto _;
assoc = auto _ };
left-inv = auto _;
right-inv = auto _ };
commute = auto _ };
*-isMonoid =
record { left-id = auto _;
right-id = auto _;
assoc = auto _ };
left-distr = auto _;
right-distr = auto _ } }