I would like to understand how to use the Ltac2 unfold tactic inside an Ltac2 function.
I know that, when proving a goal, we can use unfold lemma_name
where lemma_name is the name of a previously proven lemma, and the above tactic unfolds lemma_name in the goal.
However, I would like to create a custom function that calls the Ltac2 unfold tactic. The only way I have managed to do it is as follows:
Ltac2 my_unfold (t: constr) := unfold &t
However, when calling the above function, it returns an error of the form Anomaly found. I do not know how to call the Ltac2 unfold tactic otherwise (the purpose of the above function is to call more tactics/functions, not just the Ltac2 unfold).
The anomaly is unrelated, it’s an issue with the unfold primitive which dies when given a variable that does not exist. Please open a bug report, I will fix it when I have a bit of time.
Your example shows a confusion about the &t notation though. The t part is just a static string, so &t means that this will look for a hypothesis called t in the context. In particular, whatever term you pass to your function it will always behave the same, the t bound variable has nothing to do with &t.
The unfold tactic takes a somewhat complex type as argument. What exactly do you intend to do? You example is too trivial to give a hint.
I do not really have more “advanced examples” of where to use this. I was just “playing around” with these Ltac2 Std.v tactics, trying to figure out how they work.
I wanted to create an Ltac2 tactic that calls a function that unfolds a constr (the name of a lemma for instance) and then calls the auto tactic, or prints a message (only trivial things like this).
I saw that the Std.unfold tactic has a complex argument. I would appreciate it if you could explain to me how to construct the respective argument in this simple example, if this is possible.