Problem with \and

Stream: new members

[Husna Farooqui]

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]

Try typing \and more quickly.

[Kevin Buzzard]

It should have turned into a ∧

[Kevin Buzzard]

sorry, it's not about speed at all

[Adam Topaz]

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

[Kevin Buzzard]

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

[ROCKY KAMEN-RUBIO]

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.