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

Explain 'B_of_A' naming convention for implications 'A->B' #107

Open davidblitz opened 3 years ago

davidblitz commented 3 years ago

The naming convention is used 3 times: First time in 'Level 8: eq_zero_of_add_right_eq_self' of Advanced Addition World and then once in Advanced Multiplication World and Inequality World each. I had to ask on Zulip before I understood it so maybe it's worth explaining.

kbuzzard commented 3 years ago

Thanks. Will add something when I next have a blitz on these issues.