Documentation

Lean.Meta.Tactic.Rewrite

def Lean.MVarId.rewrite (mvarId : MVarId) (e heq : Expr) (symm : Bool := false) (config : Meta.Rewrite.Config := { transparency := Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Meta.Occurrences.all, newGoals := Meta.ApplyNewGoals.nonDependentFirst }) :

Rewrite goal mvarId

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