diff options
| author | Cyril Cohen | 2020-11-25 10:34:24 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-25 10:34:24 +0100 |
| commit | a32027b47948045c24b63645546371544a839609 (patch) | |
| tree | 7976c57a094667eb98c6ac89e6be83d63f407e4b /CHANGELOG_UNRELEASED.md | |
| parent | 7189708809e3c79effe40a2c9ecf693f66423cd3 (diff) | |
| parent | ac30dae7377f9762ceba1c5553f0542831a0bb5c (diff) | |
Merge pull request #601 from pi8027/sorting_in
Add `_in` variants of the sorting lemmas
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 90858f5..9ea88fd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -54,6 +54,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `in_on1P`, `in_on1lP`, `in_on2P`, `on1W_in`, `on1lW_in`, `on2W_in`, `in_on1W`, `in_on1lW`, `in_on2W`, `on1S`, `on1lS`, `on2S`, `on1S_in`, `on1lS_in`, `on2S_in`, `in_on1S`, `in_on1lS`, `in_on2S`. + + lemmas about interaction between `{in _, _}` and `sig`: + `in1_sig`, `in2_sig`, and `in3_sig`. - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`. @@ -270,7 +272,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). already deprecated in favor of `allpairs_rconsr`, cf renamed section). -- in `seq.v`, new lemmas `allss` and `all_mask`. +- in `seq.v`, new lemmas `allss`, `all_mask`, and `all_sigP`. + `allss` has also been declared as a hint. - in `path.v`, new lemmas `sub_cycle(_in)`, `eq_cycle_in`, `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, @@ -278,6 +281,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v`, new lemma `sort_iota_stable`. +- in `path.v`, new lemmas `order_path_min_in`, `path_sorted_inE`, + `sorted_(leq|ltn)_nth_in`, `subseq_path_in`, `subseq_sorted_in`, + `sorted_(leq|ltn)_index_in`, `sorted_uniq_in`, `sorted_eq_in`, + `irr_sorted_eq_in`, `sort_sorted_in`, `sorted_sort_in`, `perm_sort_inP`, + `all_sort`, `sort_stable_in`, `filter_sort_in`, `(sorted_)mask_sort_in`, + `(sorted_)subseq_sort_in`, and `mem2_sort_in`. + - in `seq.v` new lemmas `index_pivot`, `take_pivot`, `rev_pivot`, `eqseq_pivot2l`, `eqseq_pivot2r`, `eqseq_pivotl`, `eqseq_pivotr` `uniq_eqseq_pivotl`, `uniq_eqseq_pivotr`, `mask_rcons`, `rev_mask`, |