Closed TentativeConvert closed 2 months ago
This hint is for a trans statement, but it seems to be too cryptic:
trans
https://github.com/hhu-adam/Robo/blob/20750845be33e8e6f91b3811d264202ee0cc7b91/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean#L64
should now be obsolete (see more substantial changes introduced in 5c175781ba6a91ad0c3e2cc074b150ce43d0928d)
This hint is for a
trans
statement, but it seems to be too cryptic:https://github.com/hhu-adam/Robo/blob/20750845be33e8e6f91b3811d264202ee0cc7b91/Game/Levels/MatrixTrace/L09_EvalOnEBasis.lean#L64