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 1: unfold stdBasisMatrix kills hints #39

Open TentativeConvert opened 3 months ago

TentativeConvert commented 3 months ago

I'm not sure why anyone would want to unfold stdBasisMatrix in this level, but it turns out students do this, and then they don’t get any hints. Not sure how to deal with this. We probably do not want to add an additional branch for every single potential unfold statement in every step of every proof.

joneugster commented 3 months ago

We once had a discussion about having hints which trigger up to definitional equality, which may solve thos problem bit inteoduce others. Let's talk aboit hints on Tuesday