For tactic1 =
unfold A, B in H1 and tactic2 =
unfold A in H1, tactic1 is equal to tactic2 if we remove arguments from such tactics. Is there some word to describe
unfold … in … of the tactic, so that I can say tactic1’X is equal to tactic2’X? Maybe X can be something like “tactic structure” or something else?
Perhaps "constructor/node-kind of the node in the tactic AST"?
Last updated: Oct 04 2023 at 23:01 UTC