diff options
| author | Kazuhiko Sakaguchi | 2020-11-22 18:15:03 +0900 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-24 02:14:20 +0100 |
| commit | 95cbf3b00c2d3709b2db9cff16c321012ff4fe62 (patch) | |
| tree | 9135c5e268f2dec5ed17c2465bc4cc602b260a44 /CHANGELOG_UNRELEASED.md | |
| parent | c42c0678c5de1db9f3e747a7e3b553242719d82c (diff) | |
Add more `_in` lemmas and CHANGELOG entries
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 4de594e..542bfb3 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`, |