Commit 432120a3 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'ascii-countable' into 'master'

Add Countable instance for Ascii.ascii

See merge request iris/stdpp!154
parents 9b75ffdf bb75eecc
...@@ -11,6 +11,7 @@ API-breaking change is listed. ...@@ -11,6 +11,7 @@ API-breaking change is listed.
exported by the prelude. This is a breaking change if one only exported by the prelude. This is a breaking change if one only
imports `list.v`, but not the prelude. imports `list.v`, but not the prelude.
- Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`. - 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) ## std++ 1.3 (released 2020-03-18)
......
...@@ -115,3 +115,7 @@ Program Instance string_countable : Countable string := {| ...@@ -115,3 +115,7 @@ Program Instance string_countable : Countable string := {|
encode := string_to_pos; decode p := Some (string_of_pos p) 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. 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.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment