Accessing shadowed top-level definitions

Stream: lean4

[Jason Gross]

Is there a nice way to make this work?

structure Foo where
  foo : Type
def Foo.Unit := Foo.mk Unit
/-
3:17: application type mismatch
  { foo := Unit }
argument
  Unit
has type
  Foo
but is expected to have type
  Type
-/

Replacing Unit with Top.Unit, prelude.Unit, Init.Unit, Prelude.Unit, Init.Prelude.Unit, and Init.prelude.Unit all give me unbound identifiers

[Leonardo de Moura]

You should use _root_.Unit

[Jason Gross]

Ah, great, thanks!

[Leonardo de Moura]

We probably need a nicer syntax for this :grinning: We are still using the one used in Lean 3.

[Sebastian Ullrich]

🌲.Unit

[Leonardo de Moura]

syntax:max "🌲." noWs ident : term

macro_rules
  | `(🌲.$id:ident) =>
     return Lean.mkIdentFrom id (`_root_ ++ id.getId.eraseMacroScopes)

structure Foo where
  foo : Type

def Foo.Unit := Foo.mk 🌲.Unit