Remove parentheses from `apply (h.mp) at …` when it becomes possible

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪

https://adam.math.hhu.de

Apache License 2.0

16 stars 9 forks source link

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 8 months ago

In this level, remove the parenthesis if/when this becomes possible. Watch this discussion on Zulip for updates.

joneugster commented 8 months ago