Stream: Coq users

Topic: Describe the tactic's structure


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

view this post on Zulip Jason Gross (Jun 02 2020 at 03:40):

Perhaps "constructor/node-kind of the node in the tactic AST"?


Last updated: Jan 29 2023 at 06:02 UTC