From 5fd3709f00fdb59e8927bb886e09ea4dd00323d0 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Sun, 11 Aug 2019 15:21:19 +0100 Subject: 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 --- doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst (limited to 'doc') 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 `_, by Oliver Nash. -- cgit v1.2.3