Natural Numbers Game sorry question

Stream: new members

[Julia Scheaffer]

I am currently trying to complete the Natural numbers game, and I am getting a strange warning saying my proof uses sorry, but it does not. I am on ≤ World, Level 11/11 and this is my proof

cases hx
cases w
{ right; right; rw [h, add_zero]; rfl }
cases a
{ right; left; rw [succ_inj h] }
{ left; rw [succ_inj h] }

Which does not contain any sorry as far as I know. Is one of the tactics I'm using invoking a sorry?

[Aaron Liu]

well something's wrong with the error reporting

[Kevin Buzzard]

I dumped your proof into the plain text option for NNG and the underline-warning is on that first cases; maybe Lean doesn't like that you didn't name the variables? Changing the first line to cases hx with w hw seems to fix it.

[Aaron Liu]

succ_inj h isn't well-typed because you need to feed it the numbers first

[Julia Scheaffer]

Kevin Buzzard said:

I dumped your proof into the plain text option for NNG and the underline-warning is on that first cases; maybe Lean doesn't like that you didn't name the variables? Changing the first line to cases hx with w hw seems to fix it.

It gave the same warning when the variables did have names. But I will try that.

[Aaron Liu]

Kevin Buzzard said:

I dumped your proof into the plain text option for NNG and the underline-warning is on that first cases; maybe Lean doesn't like that you didn't name the variables? Changing the first line to cases hx with w hw seems to fix it.

that's because you broke the proof, if you put cases hx with w h it gives the same warning again

[Julia Scheaffer]

Aaron Liu said:

succ_inj h isn't well-typed because you need to feed it the numbers first

Ah, that would make sense. I was wondering why it let me use succ_inj like that, but i guess it hasnt

[Kevin Buzzard]

I am surprised you got that error though. Thanks for reporting.

[Aaron Liu]

is there an option to turn off error recovery in Elab

[Julia Scheaffer]

Unfortunate that it decided to give me no error at all :confused:

[Julia Scheaffer]

After a bit of rewriting, now I am getting errors saying my proof is incorrect. Thank you all. :smile: