Zulip Chat Archive

Stream: new members

Topic: Introduction to Lean examples

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


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:


But in my VS Code window I get an error:


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