Documentation

Lean.Elab.Tactic.Change

Implementation of the change tactic #

source
def Lean.Elab.Tactic.elabChange (e : Lean.Expr) (p : Lean.Term) :
Lean.Elab.Tactic.TacticM Lean.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