Support destructing exists with intro patterns
This is a version of !483 (closed) (by @tchajed) that uses a different approach for backwards compatibility.
The MR enables [% ...]
to be used as a pattern to destruct existentials, and (with the string-ident plugin) [%name ...]
to give a name to the witness. To maintain backwards compatibility, the same pattern can also still be used to destruct (separating) conjunctions where the left-hand side is pure. For terms that are syntactically conjunctions, this would not even require further changes (the existing IntoExist
instances already support that); but to also support ⌜φ ∧ ψ⌝
we add a new instance for convenience.
Fixes #310 (closed)
Edited by Ralf Jung