Zulip Chat Archive

Stream: new members

Topic: Problem with \and


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?

Kevin Buzzard (Jun 19 2020 at 15:48):

Try typing \and more quickly.

Kevin Buzzard (Jun 19 2020 at 15:49):

It should have turned into a

Kevin Buzzard (Jun 19 2020 at 15:49):

sorry, it's not about speed at all

Adam Topaz (Jun 19 2020 at 15:49):

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

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

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: Dec 20 2023 at 11:08 UTC