I have two questions regarding the ltac2 match! statement:

- Is it possible to insert terms into the match! 'cpattern'. I tried doing it like this,

```
From Ltac2 Require Import Ltac2 Message.
Goal 3 = 4.
let constr_3 := constr:(3) in
match! goal with
| [|- constr_3 = ?h ] => print (of_constr h)
end.
```

but this doesn't seem to work. Changing the `constr_3`

term to `$constr_3`

results in a `Unbound value constr_3`

error.

My goal being that I can use the result of a previous match statement in the next match statement.

- Is it possible to create a match pattern that extracts elements of type x? For instance, if I have a goal containing
`x`

and`y`

where`x`

and`y`

are both of type`nat`

, is there any way to create a match pattern that matches the`x`

and`y`

terms? See the following code snippet

```
From Ltac2 Require Import Ltac2 Message.
Goal 3 = 4.
(* Prints 'contains nat' *)
match! goal with
| [|- context [ nat ] ] => print (of_string "contains nat" )
| [|- _] => print (of_string "does not contain nat" )
end.
Abort.
Goal True.
(* Prints 'does not contain nat' *)
match! goal with
| [|- context [ nat ] ] => print (of_string "contains nat" )
| [|- _] => print (of_string "does not contain nat" )
end.
Abort.
```

I have tried using `context [ ?x:nat ]`

but this gives a warning `Casts are ignored in patterns [cast-in-pattern,automation]`

.

I am using Coq version 8.17.0.

Thanks in advance!

- no, see also https://github.com/coq/coq/pull/18856
- no

Didn't we have a way to include patterns into patterns though? I thought this was merged at some point.

patterns yes, terms no

But maybe patterns are sufficient, the above example doesn't discriminate enough.

Pierre-Marie Pédrot said:

But maybe patterns are sufficient, the above example doesn't discriminate enough.

Thanks for the swift response!

Out of curiosity I tried to search for the 'patterns in patterns', but I am unable to find more information on this. Could you maybe point me in the right direction?

use `pattern:(foo)`

instead of `constr:(foo)`

and `$pattern:x`

instead of `$x`

Last updated: Oct 12 2024 at 13:01 UTC