Stream: Coq users

Topic: Hint pattern beginner question


view this post on Zulip 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 O => true | _ => false 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.

view this post on Zulip 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: Jan 27 2023 at 01:03 UTC