Commit 6c89f5de authored by Robbert Krebbers's avatar Robbert Krebbers

Add missing notations on Z.

parent d8445c86
......@@ -88,6 +88,9 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ 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.
Instance Z_eq_dec: x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec: x y : Z, Decision (x y)%Z := Z_le_dec.
Instance Z_lt_dec: x y : Z, Decision (x < y)%Z := Z_lt_dec.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment