Zulip Chat Archive

Stream: lean4

Topic: merging namespaces?


view this post on Zulip 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)

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 14:57):

export foo does exactly that :)

view this post on Zulip Jason Gross (Mar 19 2021 at 14:59):

It gives me an error: expected '('

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Mar 19 2021 at 15:10):

Oh, not sure that interaction has been considered before


Last updated: May 18 2021 at 22:15 UTC