How to import notations?

Stream: lean4

[Joey Eremondi]

Is there something special I have to do to import notations defined in another file? I'm in a situation where I've got a notation defined, using the original version works fine, using the notation in the original file works fine, but using the notation in another file gives expected token.

Specifically, I've defined ▹ here: https://github.com/JoeyEremondi/lean-cwf/blob/main/LeanCwf/CwF.lean#L149

And I'm trying to use it here: https://github.com/JoeyEremondi/lean-cwf/blob/main/LeanCwf/CwF.lean#L149

I suspect I'm missing something obvious but I'm pretty stuck.

[Alex J. Best]

It should just work. In fact after some time I managed to get your project working and it does work for me. But you haven't committed the lean-toolchain file or the lake-manifest.json so I could well be using a different lean/dependencies than you. (also you should make sure the capitalization of the project is consistent, LeanCwF in Pi.lean should be LeanCwf to work properly)

[Joey Eremondi]

Ahh I feel dumb, the capital letter was indeed the problem, thanks

[Joey Eremondi]

Odd that it didn't give a "not found" error on the import, though

[Alex J. Best]

Perhaps there were some left over build files from an old version in your directiory? I definitely got not found errors when I tried it

[Mario Carneiro]

It only works on case insensitive filesystems