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.
destruct improvement with if then else
This issue to keep track of a suggestion by @bbecker to extend destruct to "if .. then .. else":
axiom H: if c1 then c2 else c3 destruct H would create two branches: one replacing H by c1 and c2 and the other one replacing it with ~c1 and c3.
Note: Similar behavior can be done for match.