diff options
| author | Oliver Nash | 2019-08-11 15:21:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-03 00:02:20 +0200 |
| commit | 8b07d47d9115905354b750e4ccc8e3efb29cd831 (patch) | |
| tree | 9f8bddbd1a5fa62d503a734c8a2430e5c4c2d399 /doc | |
| parent | 049142777e3c34faf74081842b2c363dd6462eb0 (diff) | |
New lemmas for List.v
* filter_app (moved from MSets/MSetRBT.v)
* filter_map
* filter_ext_in
* ext_in_filter
* filter_ext_in_iff
* filter_ext
* concat_filter_map
* combine_nil
* combine_firstn_l
* combine_firstn_r
* combine_firstn
* nodup_fixed_point
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst new file mode 100644 index 0000000000..9850a96e1e --- /dev/null +++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst @@ -0,0 +1,4 @@ +- New lemmas on combine, filter, and nodup functions on lists. The lemma + filter_app was moved to the List module. + + See `#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash. |