Typing mistake in the "Functional programming in Lean"?

Stream: general

[lorã]

I mean, i don't really know where should i share that and i know that's pretty small but i want to share it anyway.

So, i were reading this doc which contains this part:

image.png

If i'm not crazy today, it should'nt be "Gretting.lean" and "Gretting/Basic.lean" instead?

Thank you!

[Aaron Liu]

I think this is correct. When I made a project called "Misc", it created a file called "Misc.lean" that imports a file called "Misc/Basic.lean" which contains a simple hello world statement.

[lorã]

image.png
So it didn't create a Miscs.lean or a Miscs/Basic.lean instead, right?

[Aaron Liu]

Yes, now that I look at it again this should probably be "Greeting.lean" and "Greeting/Basic.lean"