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

Function L22_Inverse: explanation of `choose_spec` needs to be included in all branches #30

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 3 months ago

The branches that begin with

let g := fun x => (hS x).choose

do not show any hints, making it impossible to solve this level.

https://github.com/hhu-adam/Robo/blob/452a57f6ff80fb48ab3953308e56ac4ec7e5e191/Game/Levels/Function/L22_Inverse.lean#L48C7-L48C38

As noted in the level itself, unfolds also break the hints.

TentativeConvert commented 3 months ago

More changes needed to this planet. Hints in L22_Inverse should become obsolete.