Creating a new lean file

Stream: general

[Shivani Goel]

Screenshot-2023-04-09-at-6.21.52-PM.png

I am trying to create a new lean file but doesn't matter what new file I create it doesn't accept any lean commands. Can someone please guide me on how to create a new lean file. I was using the files created by @Kevin Buzzard till now. I want to create my own new file. Thanks in advance!

[Alex J. Best]

It looks like it's working ok to me, you have the info view on the right showing the output of check. What were you expecting that you didn't see so far?

[Shivani Goel]

Screenshot-2023-04-09-at-6.28.00-PM.png

I created a new file named Shivani and tried to define a constant. I don't understand why there is an error on the right?

[Shivani Goel]

I understand there is a problem with the way I am trying to define a constant. I just followed the instructions pdf. Please help me in knowing how to define a constant in lean.

[Eric Wieser]

What's the error on the first line?

[Eric Wieser]

Your screenshot only shows the second error

[Eric Wieser]

In general, all bets are off after the first error

[Eric Wieser]

(you can expand "all messages" to see all the messages at once)

[Alex J. Best]

I think the issue is that nat is spelt Nat with a capital n in Lean 4. Is the document you are looking at for lean 3 by any chance?

[Eric Wieser]

I would imagine that the error message you didn't show us makes this clear