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

Sum/Babylon: induction without named hypothesis? #25

Closed TentativeConvert closed 3 months ago

TentativeConvert commented 4 months ago

Should the line https://github.com/hhu-adam/Robo/blob/dc1bb1f6c2652384c1a0c7b638717793a440b699/Game/Levels/Sum/L06_Summary.lean#L40

be changed to 

induction m with n i_hn

? It seems that lean chooses the names “n” and “i_hn” automatically, but how stable is this behaviour? The names are used explicitly later in the proof.