Justin Kelm (Dec 07 2023 at 02:55): Justin Kelm (Dec 07 2023 at 02:55):Let's say I have a tactic for branching a match depending on the value of foo applied to the discriminee:
Ltac destruct_foo :=
match goal with | |- context[match ?d with _ => _ end] =>
let F := fresh "F" in destruct (foo d) as [F|F] end.
And let's say that now, in the context of a larger tactic that calls on destruct_foo, I want to use this hypothesis F, say to do rewrite F. In some situations I may be able to do a match goal and contextually find this hypothesis in order to use it, but in other situations hypotheses other than F will also match the syntax. Not to mention this is just inconvenient to write out each time.
Ideally, I would want something like let F := destruct_foo in rewrite F to work as expected. Is there any convenient approximation for what I want?
Paolo Giarrusso (Dec 07 2023 at 04:14):One common approach is Ltac destruct_foo tac := ... let F := fresh in destruct ...; tac F; end. then destruct_foo (fun F => rewrite F).
Paolo Giarrusso (Dec 07 2023 at 04:15):Basically, you pass to destruct_foo a function that takes "destruct_foo's" result.
Paolo Giarrusso (Dec 07 2023 at 04:19):In general, this is called continuation-passing style, if that rings a bell.
Justin Kelm (Dec 07 2023 at 05:04):Yeah, it does ring a bell, and your example is very helpful. Thank you!
Last updated: Oct 13 2024 at 01:02 UTC