Zulip Chat Archive

Stream: maths

Topic: Web Editor math


ndroock1 (May 18 2022 at 08:51):

Newbie question : how to use \R in Lean Web Editor : is it possible

Kevin Buzzard (May 18 2022 at 08:54):

\R should just work? Which of the web editors are you talking about?

ndroock1 (May 18 2022 at 08:57):

I am using https://leanprover-community.github.io/lean-web-editor/#

ndroock1 (May 18 2022 at 08:58):

using Chrome

Kyle Miller (May 18 2022 at 09:02):

It works for me in Chrome. Make sure to press space after \R

ndroock1 (May 18 2022 at 09:03):

OK Will try the space

ndroock1 (May 18 2022 at 09:09):

Does not work for me. I get a
1:16: error:
unknown identifier 'ℝ'
This time I even copied it from your example in the coursenotes on real numbers.

Eric Wieser (May 18 2022 at 09:10):

Well hang on, it sounds like typing is working just fine!

Eric Wieser (May 18 2022 at 09:10):

Did you import the file that defines docs#real?

ndroock1 (May 18 2022 at 09:13):

No I did not. How do I do that?

Kevin Buzzard (May 18 2022 at 09:15):

Ha! So when you meant "how do I make \R work" you didn't mean "how do I make the shortcut turn into ", you meant "how do I import the reals?". Try import data.real.basic at the top of your file. This has nothing to do with the web editor -- this is needed in any Lean file which uses the reals.

ndroock1 (May 18 2022 at 09:18):

And now it works! Thank you Kevin, Eric, Kyle. - I am also a Zulip newbie. Is there a way to close or accept this question or can I just leave?

Kevin Buzzard (May 18 2022 at 09:19):

Yes, you can just leave :-) Thanks for visiting!

ndroock1 (May 18 2022 at 09:21):

Bye.


Last updated: Dec 20 2023 at 11:08 UTC