From a697b20f5013abb834cd9dca3fdef2bee53221ad Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 8 Mar 2018 18:00:47 +0100
Subject: Ascii.eqb and String.eqb

---
 theories/Bool/Bool.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'theories/Bool')

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index edf78ed52d..66a82008d8 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -814,3 +814,10 @@ Defined.
 
 (** Reciprocally, from a decidability, we could state a
     [reflect] as soon as we have a [bool_of_sumbool]. *)
+
+(** For instance, we could state the correctness of [Bool.eqb] via [reflect]: *)
+
+Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b').
+Proof.
+ destruct b, b'; now constructor.
+Qed.
-- 
cgit v1.2.3