James Wood (Sep 12 2022 at 16:41): James Wood (Sep 12 2022 at 16:41):Is there a good way to make a call to a tactic embedded in an expression look like a Gallina function application, but actually behave in such a way that it slurps up all its (arbitrarily many) arguments (as untyped terms) and then runs on a goal whose type is the expected type of the entire application? I've tried writing an expression like ltac:(foo) bar baz : quux (with the intention that ltac:(foo) is eventually hidden behind a notation, so will just look normal), but this seems to result in tactic foo being applied to a goal whose type is a fresh metavariable, and I'm not sure whether foo can recover quux from that.
Gaëtan Gilbert (Sep 12 2022 at 17:31):the application needs to happen inside the ltac:()
Gaëtan Gilbert (Sep 12 2022 at 17:32):tactic notation may be able to provide variable arity but not sure
Last updated: Oct 13 2024 at 01:02 UTC