From 48b160ae9c5462f343eba10bfced8de6829a12c7 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 13 Jul 2021 10:42:57 +0900
Subject: [PATCH] add choice_of_Type definition

---
 CHANGELOG_UNRELEASED.md | 2 ++
 theories/boolp.v        | 6 ++++++
 2 files changed, 8 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ade86eb0c..ca9de461d 100644
--- 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
index 3c059dc4f..d00fa445c 100644
--- 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.