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: Oct 13 2024 at 01:02 UTC