Environment extensions

Stream: lean4

[Evgenia Karunus]

I'm trying to run the code from github.com/leanprover/lean4/~/UserExt/FooExt.lean e.g. with def hi := 5; insert_foo hi; show_foo_set;, and I get:

Lean server printed an error: libc++abi: terminating with uncaught exception of type lean::exception: cannot evaluate [init] declaration 'fooExtension' in the same module

Why does this happen/how to properly run these? (@Mario Carneiro?)

[Mario Carneiro]

that's what happens when you use an environment extension in the same module (aka file) that declares it

[Mario Carneiro]

that's why the usage code https://github.com/leanprover/lean4/blob/master/tests/pkg/user_ext/UserExt/Tst1.lean is a separate file

[Evgenia Karunus]

Is this because of the initialize keyword?