diff options
| author | Cyril Cohen | 2020-11-09 13:01:18 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-11 23:22:12 +0100 |
| commit | d84c26fa2eeeeb0029a56bac37bf1bae9f10882a (patch) | |
| tree | ab048c326c8357ca5dd59bf00db26dca64442263 /CHANGELOG_UNRELEASED.md | |
| parent | d0449f7e13f06ab7295f6919d1701e8adfa72d61 (diff) | |
Intro pattern extensions for dup, swap and apply
Diffstat (limited to 'CHANGELOG_UNRELEASED.md')
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 46ba30d..ffc1cab 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -58,6 +58,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - Added a factory `distrLatticePOrderMixin` in order.v to build a `distrLatticeType` from a `porderType`. +- Added intro pattern ltac views for dup, swap, apply: + `/[apply]`, `/[swap]` and `/[dup]`. + - in `bigop.v` new lemma `sig_big_dep`, analogous to `pair_big_dep` but with an additional dependency in the index types `I` and `J`. - in `fintype.v` adds lemma `split_ordP`, a variant of `splitP` which |