diff options
| author | Yves Bertot | 2021-01-25 11:42:04 +0100 |
|---|---|---|
| committer | GitHub | 2021-01-25 11:42:04 +0100 |
| commit | fb9fb240fe7f6a99035a4db23942cb774458d7a3 (patch) | |
| tree | 7c39005e536061079a6eb88e69b07c726be40c59 /CHANGELOG_UNRELEASED.md | |
| parent | 5853de19f08ec7ddb3782ea9bb4783fdc8443558 (diff) | |
| parent | f50852b0745b287c0ce8269752507bddd5be9fe2 (diff) | |
Merge pull request #696 from CohenCyril/sumnB
Adding lemma sumnB
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3be4138..5052e28 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). ### Added +- in `bigop.v`, added lemma `sumnB`. + - in `seq.v`, + new higher-order predicate `pairwise r xs` which asserts that the relation `r` holds for any i-th and j-th element of `xs` such that i < j. |