You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A tactic `[ t ] used in a tactic definition my_tac at line L column C in file X that is used in file Y produces output (a server message) at line L column C of file Y (independent of where the tactic my_tac was used in file Y).
A tactic
`[ t ]
used in a tactic definitionmy_tac
at lineL
columnC
in fileX
that is used in fileY
produces output (a server message) at lineL
columnC
of fileY
(independent of where the tacticmy_tac
was used in fileY
).See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Extension.20showing.20goal.20for.20a.20separate.20lemma for more information and a less cryptic description.
The text was updated successfully, but these errors were encountered: