If I have a hypothesis of the form `H : let x := exp in body`

, is there an intropattern or existing tactic that will add a definition `x := exp`

to the context and change `H`

to `H : body`

? I can do it with ltac (this seems to need the trivial match trick for beta reduction to fix up scoping):

```
Ltac split_let H := match type of H with
let x := ?e in ?Hbody => set (x:=e) in H;
change (match x with x => Hbody end) in H
end.
```

Last updated: Feb 06 2023 at 13:03 UTC