Goals accomplished 🎉

Stream: general

[Winston Yin]

Lean is fun because it gives that dopamine hit when I'm presented with "Goals accomplished :tada:". I must say that I miss the bigger, more colourful font in VSCode's Lean3 infoview, compared to the more modest and plain one in Lean4. (Very low priority) Is it possible to implement that for the Lean4 extension? I argue that it is important to be able to quickly see with the corner of one's eye if the current goal has been completed.

[Martin Dvořák]

I think we could jazz it up even more!

[Sebastian Ullrich]

In LeanInk I used my supervising authority to have :tada: swapped for :octopus: , which seemed even more fitting

[Winston Yin]

Can somebody explain the ubiquitous octopus emoji pls?

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/octopus