Boolean parameters to `MaybeFrame` and other proofmode classes are hard to read
The MaybeFrame
class used by the iFrame
tactic is defined as follows:
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
maybe_frame : □?p R ∗ Q ⊢ P.
However, as noted in !872 (merged), this progress
argument becomes quite hard to read in instances like
TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
A suggestion was to use a custom two-constructor inductive, something like
Inductive progress_indicator := DidSomething | DidNothing.
.
Operations like &&
and ||
would then need to be added for this inductive as well.
(@robbertkrebbers mentioned the MaybeFrame
instances might be removed someday, so that the MaybeFrame
class would become obsolete. That would also fix this problem.)