Documentation

Lean.Elab.Tactic.Change

Implementation of the change tactic #

source
def Lean.Elab.Tactic.elabChange (e : Expr) (p : Term) (mkDefeqError : Expr → Expr → MetaM MessageData := Lean.Elab.Tactic.elabChangeDefaultError✝) :
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.
Instances For