diff options
| author | Cyril Cohen | 2020-11-11 18:58:03 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-11 18:58:03 +0100 |
| commit | cf74596ed9f29ba4e6c125a7916f6c631366a6f3 (patch) | |
| tree | 8fcd64fa90b7aa66b402e45a8f575191e8b18bdc /CHANGELOG_UNRELEASED.md | |
| parent | afc29e48d1ab6ca572f93269a93ae4a3a68938c6 (diff) | |
| parent | 88861b5dbd2803118222fe3a020317608c4c8500 (diff) | |
Merge pull request #632 from pi8027/path-cycle-sorted
Reorganize, generalize, and add lemmas about `path`, `cycle`, and `sorted`
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6b27ef0..4b348e6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -263,6 +263,12 @@ 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 `path.v`, new lemmas `sub_cycle(_in)`, `eq_cycle_in`, + `(path|sorted)_(mask|filter)_in`, `rev_cycle`, `cycle_map`, + `(homo|mono)_cycle(_in)`. + ### Changed - in `ssrbool.v`, use `Reserved Notation` for `[rel _ _ : _ | _]` to avoid warnings with coq-8.12 @@ -334,6 +340,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). weaker hypothesis (i.e. `#|T| >= #|T'|` instead of `#|T| = #|T'|` thanks to `leq_card` under injectivity assumption). +- in `path.v`, generalized lemmas `sub_path_in`, `sub_sorted_in`, and + `eq_path_in` for non-`eqType`s. + ### Renamed - `big_rmcond` -> `big_rmcond_in` (cf Changed section) |