"wp_apply ... as"
Applying a typical spec in Iris usually looks something like this:
wp_apply (Spec with "...").
{ (* solve precondition *) }
iIntros (x) "H".
The iIntros
can be quite far removed from the wp_apply
, if proving the precondition takes some work. Also it seems a bit odd to have this separated into two tactics.
@robbertkrebbers I wonder how feasible it would be to support wp_apply (Spec with "...") as ...
, combining the iIntros
into the wp_apply
? I have actually accidentally written this last week and was a bit bummed that it did not work. ;)