Notation not continuing to override

Stream: lean4

[Brandon Brown]

For educational purposes I made my own HasAdd type class and override the default + infix notation:
infixl:65 (priority := high) " + " => HasAdd.add
It's in a namespace called nat
I save it in a file with a bunch of other nat stuff.
Then I imported it into another file and I open the nat namespace. But then if I try to use it #reduce nat.zero + nat.zero
I get an error: "failed to synthesize instance
HAdd nat nat ?m.6"

So my notation override is not persisting when I import it or am I missing something simple here?

[Daniel Selsam]

I can't reproduce this.

[Daniel Selsam]

Can you post repro?

[Brandon Brown]

I just tried to duplicate in another set of files and it's working there. I must've done something wrong along the way

[Brandon Brown]

I guess it was a visual studio code issue. I ran leanpkg build again and restarted vs code and now it's working.

[Sebastian Ullrich]

Could have been https://github.com/leanprover-community/vscode-lean4#refreshing-file-dependencies

[Kevin Buzzard]

Whenever I edit a file which is imported by another file I recompile with leanpkg build and then restart Lean, right now it seems like a sure fire way of avoiding trouble. It's so fast that it is not really an issue :-)

[Sebastian Ullrich]

I mean that works too, but you really shouldn't have to :)

[Sebastian Ullrich]

Please do complain if it doesn't work right from the editor

[Kevin Buzzard]

When I was building the algebra hierarchy I was editing three files at once and was continually having to do this. I just assumed it was normal.