def _root_.foo ?

Stream: lean4

[Jason Gross]

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]

(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]

Lean 3 just got this feature, right?

[Jason Gross]

(Someone else should answer that; I have no idea, as I haven't been tracking Lean 3)

[Kevin Buzzard]

(the answer is yes)