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

nth_rewrite #110

Open kbuzzard opened 3 years ago

kbuzzard commented 3 years ago

Apparently nth_rewrite is a tactic which people would like to see in the natural number game. I could probably get this by bumping up the Lean and mathlib versions used.