A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
16
stars
9
forks
source link
MatrixTrace, Level 8: make variable names dynamic #42
Closed
TentativeConvert closed 2 months ago
The variable
i
andj
in https://github.com/hhu-adam/Robo/blob/20750845be33e8e6f91b3811d264202ee0cc7b91/Game/Levels/MatrixTrace/L08_EvalOnEBasis.lean#L78 can have different names.