From 583c46455f321dafd56d18544b65848fbce3871d Mon Sep 17 00:00:00 2001 From: Tej Chajed <tchajed@mit.edu> Date: Thu, 13 Feb 2020 22:16:05 +0100 Subject: [PATCH] Add decidability instances for Z.gt and Z.ge --- theories/numbers.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/numbers.v b/theories/numbers.v index 0fcde178..35cc5b26 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -368,6 +368,8 @@ Proof. intros n1 n2. apply Nat2Z.inj. Qed. Instance Z_eq_dec: EqDecision Z := Z.eq_dec. Instance Z_le_dec: RelDecision Z.le := Z_le_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_lt_pi x y : ProofIrrel (x < y). Proof. unfold Z.lt. apply _. Qed. -- GitLab