1 files changed, 18 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
new file mode 100644
index 000000000..79f5393dd
--- /dev/null
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -0,0 +1,18 @@
+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 "x + y" := (addition x y).
+Class Multiplication {A B : Type} := {multiplication : A -> B -> B}.
+Notation "x * y" := (multiplication x y).
+Class Subtraction (A : Type) := {subtraction : A -> A -> A}.
+Notation "x - y" := (subtraction x y).
+Class Opposite (A : Type) := {opposite : A -> A}.
+Notation "- x" := (opposite x).
+Class Equality {A : Type}:= {equality : A -> A -> Prop}.
+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).
+\ No newline at end of file