search

impermeable / coq-waterproof

GNU Lesser General Public License v3.0
29 stars 9 forks source link

feat: Postponing choices in the Choose tactic #59

Open jim-portegies opened 2 months ago

jim-portegies commented 2 months ago

Allows for

Goal exists n : nat, n + 1 = n + 1.
Proof.
Choose n := _.
Abort.

and

Goal exists n : nat, n + 1 = n + 1.
Proof.
Choose n := ?[m].
Abort.

allowing the user to come back to these choices later.