add choice_of_Type definition

math-comp · Jul 13, 2021 · 9544e68 · 9544e68
1 parent 7b53e30
commit 9544e68
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -8,6 +8,8 @@
   + lemmas `seriesN`, `seriesD`, `seriesZ`, `is_cvg_seriesN`, `lim_seriesN`,
     `is_cvg_seriesZ`, `lim_seriesZ`, `is_cvg_seriesD`, `lim_seriesD`,
     `is_cvg_seriesB`, `lim_seriesB`, `lim_series_le`, `lim_series_norm`
+- in `boolp.v`:
+  + definitions `equality_mixin_of_Type`, `choice_of_Type`
 
 ### Changed
 

diff --git a/theories/boolp.v b/theories/boolp.v
@@ -238,6 +238,12 @@ Proof. by case: asboolP. Qed.
 Lemma asboolF (P : Prop) : ~ P -> `[<P>] = false.
 Proof. by apply/introF/asboolP. Qed.
 
+Definition equality_mixin_of_Type (T : Type) : Equality.mixin_of T :=
+  EqMixin (fun x y : T => asboolP (x = y)).
+
+Definition choice_of_Type (T : Type) : choiceType :=
+  Choice.Pack (Choice.Class (equality_mixin_of_Type T) gen_choiceMixin).
+
 Lemma is_true_inj : injective is_true.
 Proof. by move=> [] []; rewrite ?(trueE, falseE) ?propeqE; tauto. Qed.