Merge branch 'experimental/upstream' into upstream

1 files changed, 25 insertions, 0 deletions

diff --git a/plugins/setoid_ring/Algebra_syntax.v b/plugins/setoid_ring/Algebra_syntax.v
new file mode 100644
index 00000000..e896554e
--- /dev/null
+++ b/plugins/setoid_ring/Algebra_syntax.v
@@ -0,0 +1,25 @@
+
+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).
+