Web Editor math

Stream: maths

[ndroock1]

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

[Kevin Buzzard]

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

[ndroock1]

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

[ndroock1]

using Chrome

[Kyle Miller]

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

[ndroock1]

OK Will try the space

[ndroock1]

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]

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

[Eric Wieser]

Did you import the file that defines docs#real?

[ndroock1]

No I did not. How do I do that?

[Kevin Buzzard]

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]

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]

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

[ndroock1]

Bye.