Hi,

I want to match a hypothesis of the form

H: let (?x, ?y) := ?p in...

But let is ltac syntax.

How do you match let in ltac?

Thanks.

For example, this doesn't work:

```
Ltac destruct_let :=
match goal with
| [H : (let _ := ?y in _) |- _] => destruct y
end.
Definition tactest : forall p : Prop * Prop, forall z : (let (x, y) := p in x), False.
{ intros. destruct_let. }
```

`let (x, y) := p in x`

is not a let, it's just a builtin notation for `match`

thanks @Gaëtan Gilbert , but

```
Ltac destruct_let :=
match goal with
| [H : (match _ with | ?y => ?z end) |- _] => destruct y
end.
```

doesn't work either...

Last updated: Jun 13 2024 at 19:02 UTC