From bb75eecc4dca8cfaf8064b31433d2f82d6db0a66 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Thu, 30 Apr 2020 16:57:49 -0500
Subject: [PATCH] Add Countable instance for Ascii.ascii
---
CHANGELOG.md | 1 +
theories/strings.v | 4 ++++
2 files changed, 5 insertions(+)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 231e356f..0881670f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,7 @@ API-breaking change is listed.
exported by the prelude. This is a breaking change if one only
imports `list.v`, but not the prelude.
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
+- Added `Countable` instance for `Ascii.ascii`.
## std++ 1.3 (released 2020-03-18)
diff --git a/theories/strings.v b/theories/strings.v
index f83f075b..a9f2bcc5 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -115,3 +115,7 @@ Program Instance string_countable : Countable string := {|
encode := string_to_pos; decode p := Some (string_of_pos p)
|}.
Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
+Lemma ascii_of_to_digits a : ascii_of_digits (ascii_to_digits a) = a.
+Proof. by destruct a as [[][][][][][][][]]. Qed.
+Instance ascii_countable : Countable ascii :=
+ inj_countable' ascii_to_digits ascii_of_digits ascii_of_to_digits.
--
GitLab