Zulip Chat Archive

Stream: new members

Topic: Introduction to Lean examples

Nathan Temple (Sep 03 2022 at 05:06):

Hello,

I am using the example from https://leanprover.github.io/introduction_to_lean/ and when I try it on the browser in the tutorial it works fine:

image.png

But in my VS Code window I get an error:

image.png

Matt Diamond (Sep 03 2022 at 05:53):

Are you using Lean 4?

Matt Diamond (Sep 03 2022 at 05:55):

I think you might be using Lean 3 syntax with Lean 4

Last updated: Dec 20 2023 at 11:08 UTC