Jason Gross (Aug 26 2022 at 08:28): Jason Gross (Aug 26 2022 at 08:28):Is there any fundamental reason that Ltac2 Set only works when I declare the original tactic as mutable?
Jason Gross (Aug 26 2022 at 08:29):If not, I propose that "is not declared as mutable" be a warning that is fatal by default (but can be made non-fatal). I find Ltac foo ::= ... to be very useful for debugging and prototyping when I don't want to recompile all the dependencies, and would like to be able to do the same in Ltac2, even if this is strongly discouraged. (I'm even fine with this feature only working interactively and not being able to be persisted to .vo files, if need be.)
Last updated: Apr 20 2024 at 13:01 UTC