search

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

fix: improve hint in drinkers paradox #11

Closed joneugster closed 4 months ago

joneugster commented 7 months ago

https://github.com/hhu-adam/Robo/blob/580d6816fe1f515dd0baa6ce724391ab2e7eca31/Game/Levels/Predicate/L11_DrinkersParadox.lean#L61C3-L61C24

Improve the hint in the second half where rcases is needed