diff options
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5052e28..88a9d75 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,12 +20,38 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `pairwise_mask`, `pairwise_filter`, `pairwiseP`, `pairwise_all2rel`, `sub(_in)_pairwise`, `eq(_in)_pairwise`, `pairwise_map`, `subseq_pairwise`, `uniq_pairwise`, `pairwise_uniq`, and `pairwise_eq`. + + new lemmas `zip_map`, `eqseq_all`, and `eq_map_all`. - in `path.v`, new lemmas: `sorted_pairwise(_in)`, `path_pairwise(_in)`, `cycle_all2rel(_in)`, `pairwise_sort`, and `sort_pairwise_stable`. - in `interval.v`, new lemmas: `ge_pinfty`, `le_ninfty`, `gt_pinfty`, `lt_ninfty`. +- in `order.v` + + we provide a canonical total order on ordinals and lemmas + `leEord`, `ltEord`, `botEord`, and `topEord` to translate generic + symbols to the concrete ones. Because of a shortcoming of the + current interface, which requires `finOrderType` structures to be + nonempty, the `finOrderType` is only defined for ordinal which are + manifestly nonempty (i.e. `'I_n.+1`). + + new notation `Order.enum A` for `sort <=%O (enum A)`, with new + lemmas in module `Order`: `cardE`, `mem_enum`, `enum_uniq`, + `cardT`, `enumT`, `enum0`, `enum1`, `eq_enum`, `eq_cardT`, + `set_enum`, `enum_set0`, `enum_setT`, `enum_set1`, `enum_ord`, + `val_enum_ord`, `size_enum_ord`, `nth_enum_ord`, `nth_ord_enum`, + `index_enum_ord`, `mono_sorted_enum`, and `mono_unique`. + + a new module `Order.EnumVal` (which can be imported locally), with + definitions `enum_rank_in`, `enum_rank`, `enum_val` on a finite + partially ordered type `T`, which are the same as the one from + `fintype.v`, except they are monotonous when `Order.le T` is + total. We provide the following lemmas: `enum_valP`, + `enum_val_nth`, `nth_enum_rank_in`, `nth_enum_rank`, + `enum_rankK_in`, `enum_rankK`, `enum_valK_in`, `enum_valK`, + `enum_rank_inj`, `enum_val_inj`, `enum_val_bij_in`, + `eq_enum_rank_in`, `enum_rank_in_inj`, `enum_rank_bij`, + `enum_val_bij`, `le_enum_val`, `le_enum_rank_in`, and + `le_enum_rank`. They are all accessible via module `Order` if one + chooses not to import `Order.EnumVal`. ### Changed - In `ssralg.v` and `ssrint.v`, the nullary ring notations `-%R`, `+%R`, `*%R`, |