From a05d10854268f1c95337f537c2df3f6535a92979 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser <janno@mpi-sws.org> Date: Fri, 29 Jun 2018 11:45:10 +0200 Subject: [PATCH] Add `Countable` instance for `mapset`. --- theories/mapset.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/theories/mapset.v b/theories/mapset.v index 1143b152..7a497ccb 100644 --- a/theories/mapset.v +++ b/theories/mapset.v @@ -3,7 +3,7 @@ (** This files gives an implementation of finite sets using finite maps with elements of the unit type. Since maps enjoy extensional equality, the constructed finite sets do so as well. *) -From stdpp Require Export fin_map_dom. +From stdpp Require Export countable fin_map_dom. (* FIXME: This file needs a 'Proof Using' hint. *) Record mapset (M : Type → Type) : Type := @@ -76,6 +76,9 @@ Section deciders. match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); abstract congruence. Defined. + Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) := + inj_countable mapset_car (Some ∘ Mapset) _. + Next Obligation. by intros ? ? []. Qed. Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1. Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined. Global Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1. -- GitLab