Library Coq.ring.LegacyRing
Require
Export
Bool
.
Require
Export
LegacyRing_theory
.
Require
Export
Quote
.
Require
Export
Ring_normalize
.
Require
Export
Ring_abstract
.
Definition
BoolTheory
:
Ring_Theory
xorb
andb
true
false
(
fun
b
:
bool
=>
b
)
eqb
.
Defined
.
Add
Legacy
Ring
bool
xorb
andb
true
false
(
fun
b
:
bool
=>
b
)
eqb
BoolTheory
[
true
false
].