diff options
Diffstat (limited to 'plugins/setoid_ring/Algebra_syntax.v')
-rw-r--r-- | plugins/setoid_ring/Algebra_syntax.v | 18 |
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 |