Merge pull request #405 from math-comp/choice_of_Type

add choice_of_Type definition
math-comp · Jul 15, 2021 · cb9cc4c · cb9cc4c
2 parents 576856a + 48b160a
commit cb9cc4c
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
@@ -10,6 +10,8 @@
     `is_cvg_seriesB`, `lim_seriesB`, `lim_series_le`, `lim_series_norm`
 - in `classical_sets.v`:
   + lemmas `bigcup_image`, `bigcup_of_set1`
+- 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.