Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jan
stdpp
Commits
558df4bc
Commit
558df4bc
authored
Jun 02, 2021
by
Robbert Krebbers
Browse files
Update CHANGELOG regarding Permutation changes.
Thanks to
@tchajed
for pointing out the omission.
parent
8f85e406
Changes
1
Hide whitespace changes
Inline
Side-by-side
CHANGELOG.md
View file @
558df4bc
...
...
@@ -31,9 +31,11 @@ API-breaking change is listed.
-
Add tactics
`compute_done`
and
`compute_by`
for solving goals by computation.
-
Add
`Inj`
instances for
`fmap`
on option and maps.
-
Various changes to
`Permutation`
lemmas:
+
Rename
`Permutation_nil`
→
`Permutation_nil_r`
and
and
`Permutation_singleton`
→
`Permutation_singleton_r`
.
+
Add lemmas
`Permutation_nil_l`
and
`Permutation_singleton_l`
.
+
Rename
`Permutation_nil`
→
`Permutation_nil_r`
,
`Permutation_singleton`
→
`Permutation_singleton_r`
, and
`Permutation_cons_inv`
→
`Permutation_cons_inv_r`
.
+
Add lemmas
`Permutation_nil_l`
,
`Permutation_singleton_l`
, and
`Permutation_cons_inv_l`
.
+
Add new instance
`cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`
.
+
Add lemma
`Permutation_cross_split`
.
+
Make lemma
`elem_of_Permutation`
a biimplication
...
...
@@ -47,6 +49,7 @@ s/\bdecide_right\b/decide_False_pi/g
# Permutation
s/\bPermutation_nil\b/Permutation_nil_r/g
s/\bPermutation_singleton\b/Permutation_singleton_r/g
s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
' $(find theories -name "*.v")
```
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment