Tutorial world, Level 4, one single "refl," causes "Proof complete!"

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

Tutorial world, Level 4, one single "refl," causes "Proof complete!" #131

Open liusida opened 11 months ago

liusida commented 11 months ago

I was trying to understand how to use those commands, and accidentally, I put only 'refl,' into the proof, and it completed the proof, which I think doesn't make sense, right?

Level URL: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=1&level=4

Screenshot: