Library Coq.setoid_ring.Algebra_syntax
Class
Zero
(
A
:
Type
) :=
zero
:
A
.
Notation
"
0" :=
zero
.
Class
One
(
A
:
Type
) :=
one
:
A
.
Notation
"
1" :=
one
.
Class
Addition
(
A
:
Type
) :=
addition
:
A
->
A
->
A
.
Notation
"
_+_" :=
addition
.
Notation
"
x + y" := (
addition
x
y
).
Class
Multiplication
{
A
B
:
Type
} :=
multiplication
:
A
->
B
->
B
.
Notation
"
_*_" :=
multiplication
.
Notation
"
x * y" := (
multiplication
x
y
).
Class
Subtraction
(
A
:
Type
) :=
subtraction
:
A
->
A
->
A
.
Notation
"
_-_" :=
subtraction
.
Notation
"
x - y" := (
subtraction
x
y
).
Class
Opposite
(
A
:
Type
) :=
opposite
:
A
->
A
.
Notation
"
-_" :=
opposite
.
Notation
"
- x" := (
opposite
(
x
)).
Class
Equality
{
A
:
Type
}:=
equality
:
A
->
A
->
Prop
.
Notation
"
_==_" :=
equality
.
Notation
"
x == y" := (
equality
x
y
) (
at
level
70,
no
associativity
).
Class
Bracket
(
A
B
:
Type
):=
bracket
:
A
->
B
.
Notation
"
[ x ]" := (
bracket
(
x
)).
Class
Power
{
A
B
:
Type
} :=
power
:
A
->
B
->
A
.
Notation
"
x ^ y" := (
power
x
y
).