leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: prelude qulification


Kana (Feb 18 2021 at 13:57):

is there a way to get element from some prelude module, instead of local?

I want something like

def string : \nat := 0
#check prelude.string -- Type

Eric Wieser (Feb 18 2021 at 14:28):

Are you looking for _root_?

Kana (Feb 18 2021 at 15:09):

Yes, thanks!


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll