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)

changed title from Ci/ralf/exists intro pattern to Support destructing exists with intro patterns

mentioned in merge request !483 (closed)

added 1 commit

• 00a2aaaf - changelog

Compare with previous version

changed the description

Yes!!! Thanks a lot!

added 1 commit

• 9330ba95 - inline only-once-used helper functions

Compare with previous version

added 2 commits

• 1578f029 - more exist destruct test cases
• 2343a1a0 - extend proof_mode.md

Compare with previous version

added 1 commit

• 04f2e735 - replace expensive fallback instances by a specialized one that is 'good enough'

Compare with previous version

changed the description

added 4 commits

• 1342a1c1 - inline only-once-used helper functions
• 19d305e2 - more exist destruct test cases
• 0ebb29eb - extend proof_mode.md
• 171ef628 - replace expensive fallback instances by a specialized one that is 'good enough'

Compare with previous version

added 4 commits

• 5bc5ae8d - inline only-once-used helper functions
• 60649e64 - more exist destruct test cases
• a66cd0cd - extend proof_mode.md
• 5cd2995f - replace expensive fallback instances by a specialized one that is 'good enough'

Compare with previous version

added 1 commit

• 80694c14 - nits

Compare with previous version

added 1 commit

• 4f36b47a - nits

Compare with previous version