- eNew : Lean.Expr
- eqProof : Lean.Expr
- mvarIds : List Lean.MVarId
Instances For
def
Lean.MVarId.rewrite
(mvarId : Lean.MVarId)
(e heq : Lean.Expr)
(symm : Bool := false)
(config : Lean.Meta.Rewrite.Config :=
{ transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Lean.Meta.Occurrences.all,
newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst })
:
Rewrite goal mvarId
Equations
- One or more equations did not get rendered due to their size.