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

CHANGELOG.

parent 40d86146
No related branches found
No related tags found
1 merge request!277Misc improvements to `head` and `tail` functions for lists
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 0 deletions
CHANGELOG.md
+ 5
− 0
View file @ 7d8bf699
...@@ -68,6 +68,11 @@ API-breaking change is listed. ...@@ -68,6 +68,11 @@ API-breaking change is listed.
+ Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
`partial_alter_merge_r`. `partial_alter_merge_r`.
+ Drop unused `merge_assoc'` instance. + Drop unused `merge_assoc'` instance.
- Improvements to `head` and `tail` functions for lists:
+ Define `head` as notation that prints (Coq defines it as `parsing only`)
similar to `tail`.
+ Declare `tail` as `simpl nomatch`.
+ Add lemmas about `head` and `tail`.
The following `sed` script should perform most of the renaming The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
......
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