Stream: Coq users

Topic: Tactic that looks like a function


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

view this post on Zulip Gaëtan Gilbert (Sep 12 2022 at 17:31):

the application needs to happen inside the ltac:()

view this post on Zulip Gaëtan Gilbert (Sep 12 2022 at 17:32):

tactic notation may be able to provide variable arity but not sure


Last updated: Jan 29 2023 at 05:03 UTC