Skip to content
Snippets Groups Projects
Commit e99804d9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Revert "Merge branch 'byte-countable' into 'master'"

This reverts merge request !155
parent a2ac9e66
No related branches found
No related tags found
1 merge request!160Revert "Merge branch 'byte-countable' into 'master'"
......@@ -14,8 +14,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` instances for `Ascii.ascii` and `Byte.byte` from the Coq
standard library.
- Added `Countable` instance for `Ascii.ascii`.
- Make lemma `list_find_Some` more apply friendly.
## std++ 1.3 (released 2020-03-18)
......
From Coq Require Import Ascii.
From Coq Require Import Init.Byte.
From Coq Require Export String.
From stdpp Require Export list.
From stdpp Require Import countable.
......@@ -19,7 +18,6 @@ Arguments String.append : simpl never.
(** * Decision of equality *)
Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
Instance byte_eq_dec : EqDecision byte := Byte.byte_eq_dec.
Instance string_eq_dec : EqDecision string.
Proof. solve_decision. Defined.
Instance string_app_inj : Inj (=) (=) (String.append s1).
......@@ -121,5 +119,3 @@ 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.
Instance byte_countable : Countable byte :=
inj_countable Byte.to_N Byte.of_N Byte.of_to_N.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment