I'd like to use Hint Extern to match goals that consist of a match. (Goals like
match n with ... end.) I am confused how to specify the pattern for it. This looks to me like it should work based on the manual description:
#[local] Hint Extern 10 (match _ with _ => _ end) => idtac : core.
but instead it produces the following error:
Head pattern or sub-pattern must be a global constant, a section variable, an if, case, or let expression, an application, or a projection.
Isn't it using "case expression" here to mean
match? I get the same issue using
(if _ then _ else _), etc.
If I make the matched term something specific, then it's accepted. Interesting.
#[local] Hint Extern 10 (match O with _ => _ end) => idtac : core.
Ideally I'd like it to be an existential variable, though, so that I can use it in the tactic.
Last updated: Sep 30 2023 at 06:01 UTC