Skip to content

Add `iStopProof` tactic

Robbert Krebbers requested to merge robbert/istopproof into master

This commit closes issue #265 (closed).

Note that there are quite a number of ways of implementing this tactic. Right now, it will turn the proofmode sequent into a goal □ (P1 ∧ ... ∧ Pn) ∗ Q1 ∗ ... ∗ Qn ⊢ R, but one could also have distributed the s and used magic wands (i.e. turn it into a curried version).

Since the purpose of stopping the proof mode described in #265 (closed) is to use legacy tactics, I guess the non-curried version (as this MR implements) is better, since most legacy tactics cannot handle magic wands well.

Merge request reports