Advanced muit world level 4 revert

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

292 stars 73 forks source link

Advanced muit world level 4 revert #63

Closed kbuzzard closed 4 years ago

kbuzzard commented 4 years ago

This whole "revert" thing needs to be explained much better in world 9 level 4 -- it trips up a lot of people.

PatrickMassot commented 4 years ago

Don't forget that using generalizing in induction is the proper way to do it.

kbuzzard commented 4 years ago

Turns out that generalizing didn't even work with my modified induction command! Should all be fixed now (in master) and i completely rewrote the explanation