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

typo #45

Closed TentativeConvert closed 2 months ago

TentativeConvert commented 2 months ago

Shouldn’t the A in s: A → A be an Y?

https://github.com/hhu-adam/Robo/blob/387058134bdd20f0c18a1c5dfc657eec98bb7a40/Game/Levels/Cantor/L07_CantorDiag_IsFixedPt.lean#L12