diff options
| author | Oliver Nash | 2019-08-11 15:21:19 +0100 |
|---|---|---|
| committer | Oliver Nash | 2019-08-16 10:12:37 +0100 |
| commit | 5fd3709f00fdb59e8927bb886e09ea4dd00323d0 (patch) | |
| tree | 607049ca3a7277f926970a9bd75a03b426d4609a /doc | |
| parent | b8477fb38842016c226ba9d7be8f60486411a2ee (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. |