Skip to content
Snippets Groups Projects

Reserve more notation in `integers.v`.

Closed Reserve more notation in `integers.v`.
swasey/coq-stdpp:notation into master
Closed David Swasey requested to merge swasey/coq-stdpp:notation into master
Compare
and
1 file
+ 16
− 10
Compare changes
  • Side-by-side
  • Inline
theories/numbers.v
+ 16
− 10
@@ -21,6 +21,12 @@ Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Notation "x < y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y ≤ z ≤ z'"
(at level 70, y at next level, z at next level).
Reserved Infix "`div`" (at level 35).
Reserved Infix "`mod`" (at level 35).
Reserved Infix "`quot`" (at level 35).
Reserved Infix "`rem`" (at level 35).
Reserved Infix "≪" (at level 35).
Reserved Infix "≫" (at level 35).
Infix "≤" := le : nat_scope.
Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%nat : nat_scope.
@@ -30,8 +36,8 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Infix "`div`" := Nat.div : nat_scope.
Infix "`mod`" := Nat.modulo : nat_scope.
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
@@ -213,8 +219,8 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%N : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
Notation "(<)" := N.lt (only parsing) : N_scope.
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.
Infix "`div`" := N.div : N_scope.
Infix "`mod`" := N.modulo : N_scope.
Arguments N.add : simpl never.
@@ -247,12 +253,12 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (only parsing) : Z_scope.
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Infix "`div`" := Z.div : Z_scope.
Infix "`mod`" := Z.modulo : Z_scope.
Infix "`quot`" := Z.quot : Z_scope.
Infix "`rem`" := Z.rem : Z_scope.
Infix "≪" := Z.shiftl : Z_scope.
Infix "≫" := Z.shiftr : Z_scope.
Instance Zpos_inj : Inj (=) (=) Zpos.
Proof. by injection 1. Qed.