Allow pattern and type annotations in propset notation
Compare changes
Files
4- Thibaut Pérami authored
+ 2
− 0
@@ -28,6 +28,8 @@ Coq 8.19 is newly supported by this version of std++.
This allows to use patterns and type annotations in the propset
notation, Like {[ (x,y) | ... ]}
or {[ x : T | ...]}
or even {[ (x, y) : A * B | ...]}
.
However, for both the old and new notation, this notation immediately break if someone adds a binary infix |
notation downstream, In which case this will be parsed as a singleton of whatever the result of the |
operation is. This was already the case before, so anyone that did that already broke the original propset
notation