def Lean.Widget.diffInteractiveGoals (useAfter : Bool) (info : Elab.TacticInfo) (igs₁ : InteractiveGoals) :
Modifies goalsAfter with additional information about how it is different to goalsBefore.
If useAfter is true then igs₁ is the set of interactive goals after the tactic has been applied.
Otherwise igs₁ is the set of interactive goals before.
Equations
- One or more equations did not get rendered due to their size.