Stream: Ltac2

Topic: Matching subexpression of the goal

Tomaz Gomes (Jul 25 2024 at 16:13):

Hi,

In the following example, is there a way to name the subexpression (match _ with _ => _ end) so I can have access to it?

Ltac2 foo () :=
  match! goal with
  | [ |- context c[ (match ?x with _ => _ end) ]] =>
     printf "%t" x
   end.

Something like:

  | [ |- context c[ (match ?x with _ => _ end) as ?name ]] =>

Théo Winterhalter (Jul 26 2024 at 12:03):

You could always do it in two steps, even if that's not really elegant: you match on context c[ ?name ] and then on name. I don't know what that changes in terms of efficiency though (I'm guessing it can only be worse).

Tomaz Gomes (Jul 26 2024 at 12:24):

Thanks! That makes sense. I am wondering whether the decrease in efficiency will be too high, since we will match on every possible term inside the context and fail on most of them

Théo Winterhalter (Jul 26 2024 at 12:26):

Yes, I've been wondering the same myself.

Last updated: Oct 12 2024 at 12:01 UTC