diff options
| author | Enrico Tassi | 2020-09-03 15:52:42 +0200 |
|---|---|---|
| committer | GitHub | 2020-09-03 15:52:42 +0200 |
| commit | d3950a35fe2e901d92335ae9c05562b14d049214 (patch) | |
| tree | 14399b0457c7969013e6978645fc6866db5fe9e1 /CHANGELOG_UNRELEASED.md | |
| parent | 5618ef0dae970a40a2d44f06966560659450c6ae (diff) | |
| parent | b81aa92716bcd19fa364911f5efaf5d0155d9376 (diff) | |
Merge pull request #558 from CohenCyril/are_allpairs
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 db6e18b..5a394b5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,6 +51,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `pinvmx_free`, and `pinvmx_full`. - 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 |