Zulip Chat Archive

Stream: lean4

Topic: merging namespaces?

Jason Gross (Mar 19 2021 at 14:55):

Is there a way to merge namespaces? (Really the feature that I want is for open foo to be attached to a namespace, so that as soon as I open the namespace, foo is also opened)

Sebastian Ullrich (Mar 19 2021 at 14:57):

export foo does exactly that :)

Jason Gross (Mar 19 2021 at 14:59):

It gives me an error: expected '('

Sebastian Ullrich (Mar 19 2021 at 15:02):

Ah. It only works with an explicit list of identifiers to be exported in Lean 4.

export MonadEnv (getEnv modifyEnv)

Jason Gross (Mar 19 2021 at 15:03):

What if the things I want to export are just the scoped attributes and syntax rules / notations / unification hints?

Jason Gross (Mar 19 2021 at 15:04):

Hm, export Foo (some_instance) does not seem to export the fact that some_instance is an instance

Sebastian Ullrich (Mar 19 2021 at 15:10):

Oh, not sure that interaction has been considered before

Last updated: Dec 20 2023 at 11:08 UTC