Stream: Coq users

Topic: Move let in hypothesis to definition in context

Brandon Moore (Jun 30 2021 at 21:25):

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: Apr 20 2024 at 12:02 UTC