Zulip Chat Archive

Stream: lean4

Topic: def _root_.foo ?


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

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

view this post on Zulip Eric Wieser (Mar 19 2021 at 14:46):

Lean 3 just got this feature, right?

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

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 15:51):

(the answer is yes)


Last updated: May 18 2021 at 22:15 UTC