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

recursion break #125

Open orhid opened 2 years ago

orhid commented 2 years ago

in level 2 of advanced addition world I foolishly did repeat {apply succ_inj} which I suppose went into a recursive loop and broke the game, after some time I got a new kind of error failed to synthesize type class instance for a b : mynat, h : succ (succ a) = succ (succ b) ⊢ has_bind nat_num_game which as far as I can see is unrecoverable from without resetting the game

kbuzzard commented 2 years ago

Wow that last one is impressive! Do you remember how you managed to get it?

orhid commented 2 years ago

i believe just the repeat instruction did that, though I do not remember exactly