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:
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):
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: May 18 2021 at 22:15 UTC