diff options
| -rw-r--r-- | CHANGELOG.md | 7 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 7 |
2 files changed, 7 insertions, 7 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md index 1cdf035..f8c3221 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,13 +29,6 @@ versions may be dropped. - computing (efficiently) (item, multiplicity) tallies of sequences over an `eqType`: `tally s`, `incr_tally bs x`, `bs \is a wf_tally`, `tally_seq bs`. -- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, - `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. - -- Bigop theorems: `big_rmcond`, `bigD1_seq`, - `big_enum_val_cond`, `big_enum_rank_cond`, - `big_enum_val`, `big_enum_rank`, `big_set`. - ### Changed - definition of `PredType` which now takes only a `P -> pred T` function; diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ee236d9..c03b4f8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -23,6 +23,13 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added theorems `flatten_map1` and `allpairs_consr` in `seq.v`. +- Fintype theorems: `fintype0`, `card_le1P`, `mem_card1`, + `card1P`, `fintype_le1P`, `fintype1`, `fintype1P`. + +- Bigop theorems: `big_rmcond`, `bigD1_seq`, + `big_enum_val_cond`, `big_enum_rank_cond`, + `big_enum_val`, `big_enum_rank`, `big_set`. + ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to |