Skip to content
Snippets Groups Projects

Allow pattern and type annotations in propset notation

Merged Thibaut Pérami requested to merge tperami/stdpp:propsetbinder into master
4 files
+ 28
1
Compare changes
  • Side-by-side
  • Inline
Files
4
+ 2
0
@@ -28,6 +28,8 @@ Coq 8.19 is newly supported by this version of std++.
to refer to a hypothesis on the goal (`inv 1`).
- Add `prod_swap : A * B → B * A` and some basic theory about it.
- Add lemma `join_app`.
- Allow patterns and type annotations in `propset` notation, e.g.,
`{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
The following `sed` script should perform most of the renaming
(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
Loading