VScode not showing an error

Stream: new members

[Robert Watson]

Exactly, when there is an error it doesn't always produce an error: that's the error! Sometimes it does, sometimes it doesn't. It's hit and miss. But I don't yet know why.

[Patrick Massot]

I'm afraid there is nothing we can do to help you without a mwe.

[Mauricio Collares]

Can you post a screenshot?

[Robert Watson]

On the Natural Numbers Game, advanced addition world 13/13. I am not trying to complete it though, I've done that. This is more or less an mwe just to illustrate a really simple question:

intro f,
have add_one : (n + 1 = succ n) := add_one_eq_succ n,
have add_one2 : (succ n = n + 1) := (add_one),
rw (add_one2) at f,

The query:

Is there a way to do this in one tactic USING add_one_eq_succ n? eg rw (←add_one_eq_succ n) at f RATHER THAN using the 'different' tactic succ_eq_add_one? What I mean is...if a tactic is of the form a = b, then how do you do a rw using b = a without having to prove b = a from a = b? Is there a simple syntax for that?

That's all the question is!

[Jireh Loreaux]

My guess with no context: you are missing a right brace somewhere.