liao zhang (May 31 2020 at 12:53): liao zhang (May 31 2020 at 12:53):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?
Jason Gross (Jun 02 2020 at 03:40):Perhaps "constructor/node-kind of the node in the tactic AST"?
Last updated: Apr 19 2024 at 22:01 UTC