Zulip Chat Archive

Stream: lean4

Topic: Accessing shadowed top-level definitions


view this post on Zulip Jason Gross (Mar 05 2021 at 19:39):

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

view this post on Zulip Leonardo de Moura (Mar 05 2021 at 19:40):

You should use _root_.Unit

view this post on Zulip Jason Gross (Mar 05 2021 at 19:41):

Ah, great, thanks!

view this post on Zulip Leonardo de Moura (Mar 05 2021 at 19:41):

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

view this post on Zulip Sebastian Ullrich (Mar 05 2021 at 19:43):

🌲.Unit

view this post on Zulip Leonardo de Moura (Mar 05 2021 at 19:54):

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

Last updated: May 07 2021 at 13:21 UTC