Stream: Ltac2

Topic: `Ltac2 Set` on non-mutable Ltac2 definitions


view this post on Zulip 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?

view this post on Zulip 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: Jan 31 2023 at 11:01 UTC