aboutsummaryrefslogtreecommitdiff
path: root/CHANGELOG_UNRELEASED.md
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
-rw-r--r--CHANGELOG_UNRELEASED.md2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1e779c3..839e796 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 `ssrnat.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.