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.