diff --git a/lifetime/lifetime_sig.v b/lifetime/lifetime_sig.v index 06af32be7f4594d08bccf4cbd334b1dc3bc0e209..451a072702ec9df4d95db5d451c338cd3b3ad760 100644 --- a/lifetime/lifetime_sig.v +++ b/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]. diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v index 89a416dba92cae485c1cb21ec88b53e07bfc32ea..6f00d3d21635ed0968df09797e6a07edd5520ac5 100644 --- a/lifetime/model/definitions.v +++ b/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 := _. diff --git a/lifetime/model/primitive.v b/lifetime/model/primitive.v index 3fd9472c74ec87e79e86d38b8b0386a63be1ef1e..a9104e8f19a8c5eba7c872b4893a81af7ac612ee 100644 --- a/lifetime/model/primitive.v +++ b/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 (κ ⊓.) := _.