Topic: def _root_.foo ?
Jason Gross (Mar 19 2021 at 14:16):
Could there be support for
def _root_.foo? I want to be able to put things in namespaces that are not children of the current namespace, without closing the current section. e.g.
namespace foo section variable (a b c d : Nat) def some_complicated_proof : a = b := sorry def _root_.bar : a = b := some_complicated_proof a b end end foo #print bar -- unknown constant 'bar'
Jason Gross (Mar 19 2021 at 14:41):
(Should I make an issue for this feature request? In general I'm not sure whether to request things here or on the issue tracker.)
Eric Wieser (Mar 19 2021 at 14:46):
Lean 3 just got this feature, right?
Jason Gross (Mar 19 2021 at 14:53):
(Someone else should answer that; I have no idea, as I haven't been tracking Lean 3)
Kevin Buzzard (Mar 19 2021 at 15:51):
(the answer is yes)
Last updated: May 18 2021 at 22:15 UTC