Karl Palmskog (Mar 24 2022 at 08:03): Karl Palmskog (Mar 24 2022 at 08:03):In SSReflect, by [] is preferred over running the equivalent done by itself. This enables having all proof scripts subgoals end in by ....
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?
Paolo Giarrusso (Mar 24 2022 at 08:27):In stdpp, that's correct
Paolo Giarrusso (Mar 24 2022 at 08:29):And as you imply, loading ssreflect lets you "fix" that, but some tweaks are "recommended"
Paolo Giarrusso (Mar 24 2022 at 08:33): Paolo Giarrusso (Mar 24 2022 at 08:35):Stdpp also has a notation for by tactic, but not the brace variant:
Karl Palmskog (Mar 24 2022 at 08:44):right, so I guess I have to define the brace variant by myself then (I'd like to avoid mixing Stdpp and SSR)
Paolo Giarrusso (Mar 24 2022 at 10:20):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: Oct 13 2024 at 01:02 UTC