Zulip Chat Archive

Stream: new members

Topic: Problem with \and


view this post on Zulip Husna Farooqui (Jun 19 2020 at 15:48):

Hi, I'm an absolute beginner with Lean. Before this, I was using the Lean web editor while following the "Logic and Proof" and the "Theorem Proving in Lean" guides. I just downloaded Lean onto my computer by following the Windows instructions on the Lean community page.

But after trying it out, I have a problem with using \and:
Problem-with-and.PNG

Does anybody know how I can fix this?

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:48):

Try typing \and more quickly.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:49):

It should have turned into a

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:49):

sorry, it's not about speed at all

view this post on Zulip Adam Topaz (Jun 19 2020 at 15:49):

isn't it more of an issue about inserting a space at the right time?

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:50):

Delete \and and try typing it again -- press tab or space at the end and it should turn into the symbol

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 19 2020 at 19:49):

I've found VSCode also doesn't recognize macros if you add the the \ after typing the word. Sometimes it also lags a little and looks like it isn't recognizing it but is just thinking (especially if the file is big and is also taking a while to compile). Also want to second that it it might not become anything until you hit space after the word.


Last updated: May 11 2021 at 23:11 UTC