Lean.Elab.Tactic.Conv.Change

Equations

Lean.Elab.Tactic.Conv.evalChange stx = let discr := stx; if Lean.Syntax.isOfKind discr `Lean.Parser.Tactic.Conv.change = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr := Lean.Syntax.getArg discr 1; let e := discr; do let lhs ← Lean.Elab.Tactic.Conv.getLhs let a ← Lean.getMCtx let mvarCounterSaved : Nat := a.mvarCounter let a ← liftM (Lean.Meta.inferType lhs) let r ← Lean.Elab.Tactic.elabTermEnsuringType e (some a) false let a ← liftM (Lean.Meta.getMVars r) let a ← liftM (Lean.Elab.Tactic.filterOldMVars a mvarCounterSaved) Lean.Elab.Tactic.logUnassignedAndAbort a let a ← liftM (Lean.Meta.isDefEqGuarded r lhs) let _do_jp : PUnit → Lean.Elab.Tactic.TacticM Unit := fun y => Lean.Elab.Tactic.Conv.changeLhs r if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.throwError (Lean.toMessageData "invalid 'change' conv tactic, term" ++ Lean.toMessageData (Lean.indentExpr r) ++ Lean.toMessageData "\nis not definitionally equal to current left-hand-side" ++ Lean.toMessageData (Lean.indentExpr lhs) ++ Lean.toMessageData "") _do_jp y else let discr := stx; Lean.Elab.throwUnsupportedSyntax