# Additional declarations for `Lean.Meta.Tactic.Rewrite` #

source
def Lean.Expr.rewrite (e eq : Expr) :
MetaM Expr

Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

Equations

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

Instances For

source
def Lean.Expr.rewriteType (e eq : Expr) :
MetaM Expr

Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.

Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

Equations

- e.rewriteType eq = do let __do_lift ← Lean.Meta.inferType e let __do_lift ← __do_lift.rewrite eq Lean.Meta.mkEqMP __do_lift e

Instances For