Stream: Coq users

Topic: Guarding ltac matches with tests


view this post on Zulip Ricardo Almeida (May 10 2024 at 08:58):

Hi, I'm trying to guard some ltac matches with tests. I thought using an actual guard would do it but no success yet. For instance

Goal (2=2).
  match goal with
  | |- ?n = 2 => idtac n; guard n=2; reflexivity
  end.

gives the error Ltac variable n is bound to a value of type constr which cannot be coerced to an integer. Any suggestions on how to do this?

view this post on Zulip Gaëtan Gilbert (May 10 2024 at 09:33):

use constr_eq if you're comparing terms, not guard

view this post on Zulip Ricardo Almeida (May 10 2024 at 11:16):

Thanks. And I guess that if I want to do, say, compare 3 with 2+1, it doesn't work since they're not actually the same term:

Goal (3=2+1).
    match goal with
    | |- ?n = ?m+1 => idtac n; constr_eq n (m+1); reflexivity
    end.

Last updated: Jun 22 2024 at 14:01 UTC