Zulip Chat Archive

Stream: new members

Topic: symmetry of a theorem

Robert Watson (Feb 25 2022 at 18:02):

I'm wondering if there is an easier way to write this:

have add_one : (a' + 1 = succ a') := add_one_eq_succ a',
have add_one2 : (succ a' = a' + 1) := (add_one),
rw (add_one2) at f,

Like for example:

rw (←add_one_eq_succ a') at f,

So far I haven't been able to get the syntax right for this.

Kevin Buzzard (Feb 25 2022 at 18:39):

Can you post a #mwe ?

Robert Watson (Feb 28 2022 at 07:59):

When I try to do lean in VSCode I find that it often produces the following even when there is an error in the code, or even if the code is absurd (see lack of errors below)...so I can't do a proper mwe right now. I have to use the Natural Numbers Game online which works, but that isn't a real mwe, so I'll do it using that:

All Messages (1)
No messages.

Riccardo Brasca (Feb 28 2022 at 09:18):

There is no error/picture in your message.

Last updated: Dec 20 2023 at 11:08 UTC