by  is preferred over running the equivalent
done by itself. This enables having all proof scripts subgoals end in
Stdpp provides a standalone analogue to
done, but seemingly it's not possible to do
by  using only Stdpp. Is the Stdpp idiom to only write
done when one wants to run
done by itself?
In stdpp, that's correct
And as you imply, loading ssreflect lets you "fix" that, but some tweaks are "recommended"
Stdpp also has a notation for
by tactic, but not the brace variant:
right, so I guess I have to define the brace variant by myself then (I'd like to avoid mixing Stdpp and SSR)
All of iris uses that mix of course, but YMMV. I'd guess you can define this shortcut easily, but you probably can't define
by [tac1 | tac2] and variants without a plugin.
Last updated: Feb 01 2023 at 11:04 UTC