search

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

Undocumented implicit variables in Advanced Addition World #102

Open darijgr opened 4 years ago

darijgr commented 4 years ago

lean-1 At least I think these are implicit variables, with different levels of implicitness? I find them pretty confusing, as these are theorems that do need to be instantiated with explicit arguments (or one gets ?m_1 type parameters, which are not explained in the game), and I don't know how to instantiate implicit variables. Worth changing or explaining.