Skip to content
Snippets Groups Projects
Commit b5a66ffb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'z-greater-decidability' into 'master' 

Add decidability instances for Z.gt and Z.ge

See merge request iris/stdpp!110
parents 355c84cf 583c4645
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 0 deletions
theories/numbers.v
+ 2
− 0
View file @ b5a66ffb
...@@ -368,6 +368,8 @@ Proof. intros n1 n2. apply Nat2Z.inj. Qed. ...@@ -368,6 +368,8 @@ Proof. intros n1 n2. apply Nat2Z.inj. Qed.
Instance Z_eq_dec: EqDecision Z := Z.eq_dec. Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
Instance Z_le_dec: RelDecision Z.le := Z_le_dec. Instance Z_le_dec: RelDecision Z.le := Z_le_dec.
Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec. Instance Z_lt_dec: RelDecision Z.lt := Z_lt_dec.
Instance Z_ge_dec: RelDecision Z.ge := Z_ge_dec.
Instance Z_gt_dec: RelDecision Z.gt := Z_gt_dec.
Instance Z_inhabited: Inhabited Z := populate 1. Instance Z_inhabited: Inhabited Z := populate 1.
Instance Z_lt_pi x y : ProofIrrel (x < y). Instance Z_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Z.lt. apply _. Qed. Proof. unfold Z.lt. apply _. Qed.
......
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