ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
Apache License 2.0
288 stars 72 forks source link

Some solutions use `assumption` which isn't mentioned in the text #99

Open Julian opened 4 years ago

Julian commented 4 years ago

(New user here as well, so apologies for brutal errors).

I had to cheat on e.g. World 9 Level 4, which I saw uses the assumption tactic which I don't think was explained in the text.

I looked it up in the documentation but maybe either the tactic should be introduced somewhere or the solution replaced to use the actual hypothesis being applied so that those who've only gone through the game and nothing further can follow it?

Happy to send a PR if so.