Additional declarations for Lean.Meta.Tactic.Rewrite

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.

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