diff options
| author | coqbot-app[bot] | 2021-03-26 07:39:41 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-26 07:39:41 +0000 |
| commit | 71453f1643b55679d44caee30ce5541b5aa47263 (patch) | |
| tree | 572b79953b061add3abc814c0ad97a2552b388a3 /doc | |
| parent | 16d9e9cf378b9eb0ee0fc42c5c0a3a23b3df6ff4 (diff) | |
| parent | 680ffd88630ac7f630533ce33d19200b8669f34a (diff) | |
Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmas
Reviewed-by: olaure01
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/13955-List_lemmas1.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/10-standard-library/13955-List_lemmas1.rst b/doc/changelog/10-standard-library/13955-List_lemmas1.rst new file mode 100644 index 0000000000..73eb9a78d9 --- /dev/null +++ b/doc/changelog/10-standard-library/13955-List_lemmas1.rst @@ -0,0 +1,4 @@ +- **Added:** + Lemmas to ``List``: ``Exists_map``, ``Exists_concat``, ``Exists_flat_map``, ``Forall_map``, ``Forall_concat``, ``Forall_flat_map``, ``nth_error_map``, ``nth_repeat``, ``nth_error_repeat`` + (`#13955 <https://github.com/coq/coq/pull/13955>`_, + by Andrej Dudenhefner, with help from Olivier Laurent). |