Zulip Chat Archive

Stream: mathlib4

Topic: No goals

Johan Commelin (Jun 20 2023 at 07:02):

I guess this has been discussed before, but can we change the "No goals" message to "Goals accomplished :tada:" in mathlib 4?

Patrick Massot (Jun 20 2023 at 07:19):

I don't think we should do that before we get a non-confusing tactic state display. This has been discussed a lot already.

Patrick Massot (Jun 20 2023 at 07:21):

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/premature.20.22goals.20accomplished.22

Johan Commelin (Jun 20 2023 at 07:28):

Agreed -- thanks for reminding me of that discussion

Last updated: Dec 20 2023 at 11:08 UTC