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 : 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: Oct 03 2023 at 04:02 UTC