Malcolm Sharpe (Aug 31 2022 at 19:55): Malcolm Sharpe (Aug 31 2022 at 19:55):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.
Malcolm Sharpe (Aug 31 2022 at 20:01):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