can't get lean4-samples to work

Stream: new members

[SwollenBerks]

opened the HelloWorld samples in the lean4-samples repo and this is the error I get image.png
this is the file it seems to be complaining about
image.png

[Kevin Buzzard]

You might want to ask this in the #lean4 stream, that's where most of the lean 4 users hang out

[Kevin Buzzard]

And you can post code within triple #backticks which makes it much easier to read and copy/paste.

[Andrés Goens]

that is kind of strange, maybe @Mac, who develops Lake, knows what's happening there?

[Mac]

@SwollenBerks what version of Lean are you running? (You can figure this out by run lean --version in a terminal / command prompt within the sample directory).

[Mac]

It seems to me like your nightly may be out of date. (You can update it by running elan update leanprover/lean4:nightly.)