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

documentation of `constructor` tactic should mention iff statements #41

Closed TentativeConvert closed 2 months ago

TentativeConvert commented 2 months ago

done: 0e5faa7fa0249750a6f1980c9d785d6122b545cb