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: Dec 20 2023 at 11:08 UTC