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

Advanced Addition World, Level 11: add_right_eq_zero #76

Closed trj2059 closed 4 years ago

trj2059 commented 4 years ago

If you enter in.

induction a with d hd, intro h, refl, intro h, rw succ_add at h, exfalso, apply (succ_ne_zero (d+b)) at h, exact h,

You will get "no goals".

To get "Proof Complete"

Change this line.

apply (succ_ne_zero (d+b)) at h,

To

apply (succ_ne_zero (d+b)),

I don't know if this is a bug in the lean parser, but it doesn't seem like proper behavior.

kbuzzard commented 4 years ago

You might get "no goals" but you also get an error in the error box; "apply ... at ..." is not valid syntax.