Hi all,

Is such thing possible? E.g.

```
Goal 1 = let n := 1 in n.
match goal with
| [ |- context[let _ in _] ] => idtac "let";
| _ => idtac "nope"
end.
```

Ltac has its own `let`

construct, I guess that is the problem.

Is there anything like `constr:`

which could be specified in order to get Gallina's `let`

matched?

You just need to add the `:=`

of the `let`

in the pattern, and it works (also remove the trailing `;`

after `"let"`

):

```
Goal 1 = let n := 1 in n.
match goal with
| [ |- context[let _ := _ in _] ] => idtac "let"
| _ => idtac "nope"
end.
```

Thanks @Kenji Maillard! That makes sense :smile:

Is there any reason why this match wouldn't work?

```
Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in ?Z] ] => idtac "let"
| _ => idtac "nope"
end.
```

But this match works:

```
Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in _] ] => idtac "let"
| _ => idtac "nope"
end.
```

The value to be bound by `Z`

depends on `X`

so that might explains why it does not work in the first case.

With 2nd order pattern matching it seems to work fine:

```
Goal 10 = let n := 1 in (n + 9).
match goal with
| [ |- context[ let X := ?V in @?Z X] ] => idtac "let"
| _ => idtac "nope"
end.
```

Kenji Maillard said:

The value to be bound by

`Z`

depends on`X`

so that might explains why it does not work in the first case.

With 2nd order pattern matching it seems to work fine:`Goal 10 = let n := 1 in (n + 9). match goal with | [ |- context[ let X := ?V in @?Z X] ] => idtac "let" | _ => idtac "nope" end.`

Wow! Will read more about 2nd order capabilities. Thanks again @Kenji Maillard :smile:

Nikola Katić has marked this topic as resolved.

Last updated: Oct 04 2023 at 21:01 UTC