lft is EqDecision and Countable

lifetime/lifetime_sig.v

@@ -65,7 +65,16 @@ Module Type lifetime_sig.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
+  Global Declare Instance lft_eq_dec : EqDecision lft.
+  Global Declare Instance lft_countable : Countable lft.
+
+  Global Declare Instance atomic_lft_inhabited : Inhabited atomic_lft.
+  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
+  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
+
   Global Declare Instance bor_idx_inhabited : Inhabited bor_idx.
+  Global Declare Instance bor_idx_eq_dec : EqDecision bor_idx.
+  Global Declare Instance bor_idx_countable : Countable bor_idx.
 
   Global Declare Instance lft_intersect_comm : Comm (A:=lft) eq (⊓).
   Global Declare Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓).
@@ -110,8 +119,6 @@ Module Type lifetime_sig.
   Global Declare Instance atomic_lft_to_lft_inj : Inj eq eq atomic_lft_to_lft.
   Global Declare Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 
-  Global Declare Instance atomic_lft_eq_dec : EqDecision atomic_lft.
-  Global Declare Instance atomic_lft_countable : Countable atomic_lft.
 
   (** * Laws *)
   Parameter lft_tok_sep : ∀ q κ1 κ2, q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].

lifetime/model/definitions.v

@@ -353,6 +353,7 @@ Qed.
 Global Instance positive_to_atomic_lft_inj : Inj eq eq positive_to_atomic_lft.
 Proof. apply _. Qed.
 
+Global Definition atomic_lft_inhabited : Inhabited atomic_lft := _.
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
 

lifetime/model/primitive.v

@@ -303,7 +303,11 @@ Qed.
 
 (** Basic rules about lifetimes  *)
 Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance lft_eq_dec : EqDecision lft := _.
+Local Instance lft_countable : Countable lft := _.
 Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance bor_idx_eq_dec : EqDecision bor_idx := _.
+Local Instance bor_idx_countable : Countable bor_idx := _.
 Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
 Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.