Can't write "use (succ(succ a))"

[VasiliPupkin256]

Goal: y ≤ y + succ (succ a)

I've had to go the long way use (a+2) rw [two_eq_succ_one] rw [one_eq_succ_zero] repeat rw [add_succ] rw [add_zero] rfl

Instead of just typing use (succ(succ a)) which is not allowed. PS: one can type use (succ a) though.

[joneugster]

I need some context :) Which game/level were you playing, NNG?

Is it more than just adding a space between succ and (, i.e. succ ( instead of succ(?

[VasiliPupkin256]

It was Level 8 Inequality World. Yes, adding a space solved the issue. The parser is odd.

[joneugster]

Yes Im afraid this might be just how Lean works: its oddly whitespace sensitive although it gives the impression its not.