The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
Choose syntax and implement destructuring existentials with pure components, following !400
It'd be nice to support something like iDestruct "H" as "∃[%x HP]" on "H": ∃ x, P (where the ∃[ipat ipat] syntax is a strawman), mapping that introduction pattern to iExistsDestruct. The killer feature is support for nested existentials, which require multiple iDestruct calls today.
In discussion on !400 (merged), I and @tchajed considered supporting that with pattern [%x HP], but that pattern is already mapped to iAndDestruct, and unlike in Coq the two methods are very different.
Steps:
- bikeshed a syntax
- any other discussion on the specification, if needed
- implement this.