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
288 stars 72 forks source link

Minor typo in World 10 Lvl 1 #121

Open milescalabresi opened 2 years ago

milescalabresi commented 2 years ago

The world introduces the \exists symbol as "upside-down E" but probably should be "backwards E". Very minor nit, but just adding polish to an excellent level