Implementation of the change tactic

def Lean.Elab.Tactic.elabChange (e : Expr) (p : Term) : TacticM Expr

Elaborates the pattern p and ensures that it is defeq to e. Emulates (show p from ?m : e), returning the type of ?m, but e and p do not need to be types. Unlike (show p from ?m : e), this can assign synthetic opaque metavariables appearing in p.

Equations

• One or more equations did not get rendered due to their size.