Predicate/Quantus, Level 10: add additional warning about branch not yet covered

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

Predicate/Quantus, Level 10: add additional warning about branch not yet covered #24

Closed TentativeConvert closed 4 months ago

TentativeConvert commented 4 months ago

Players that start with unfold Odd, push_neg get a warning “Dieser Lösungsweg scheint mir zu schwierig …”. Players that start with push_neg, unfold Odd do not get that warning. I suppose that this latter approach is equally difficult. (I haven’t check this in detail, but I was only able to finish from here using the have tactic, which is not unlocked at this point.)

joneugster commented 4 months ago

added the hint again after

push_neg
unfold Odd
intro n

that way it catches a unfold after intro too.