diff options
| author | Cyril Cohen | 2020-08-22 00:00:41 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 14:16:33 +0200 |
| commit | b81aa92716bcd19fa364911f5efaf5d0155d9376 (patch) | |
| tree | 81dbc5ec9cb6cfd9ecb724302960ac079f0d39a3 /CHANGELOG_UNRELEASED.md | |
| parent | b392a135a5f69a91526ce8004bb29659ef4be511 (diff) | |
Adding allrel predicate
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3347f21..922a689 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -42,6 +42,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). coefficient. - in `poly.v`, new lemma `commr_horner`. +- in `seq.v`, new lemma `mkseqP` to abstract a sequence `s` with + `mkseq f n`, where `f` and `n` are fresh variables. + +- in `seq.v`, new high-order predicate `allrel r s` which + asserts that a relation `r` holds on all pairs of elements of `s`, and + + lemmas `allrel_map`, `allrelP` and `allrel0`. + + lemmas `allrel1`, `allrel2` and `allrel_cons`, + under assumptions of reflexivity and symmetry of `r`. ### Changed |