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

Robotswana 9: rename variable, align hint with proof #35

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 3 months ago

The use of the variable i in the hint at https://github.com/hhu-adam/Robo/blob/2fff9106b1e4610acb25dd09d4dfd2e4319ac95a/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean#L56 is unfortunate as it clashes with the fixed i already introduced earlier (at least for humans). Also, this hint does not coincide with the actual command used in the proof (see next line). I'm not sure whether the command in the hint is more efficient or the command in the proof is more efficient.