Zulip Chat Archive

Stream: new members

Topic: Definition of {a,b}


view this post on Zulip Thomas Browning (Aug 21 2020 at 22:17):

We're having trouble finding the definition of a set {a,b} (presumably in terms of set.insert). Does anyone know where it is?

view this post on Zulip Reid Barton (Aug 21 2020 at 22:21):

If you mean the definition of the notation, it's in C++ somewhere

view this post on Zulip Reid Barton (Aug 21 2020 at 22:22):

If you just want to know what the definition is, probably #reduce will help.

view this post on Zulip Thomas Browning (Aug 21 2020 at 22:29):

oh, you think it's in C++ rather than lean?

view this post on Zulip Bryan Gin-ge Chen (Aug 21 2020 at 22:31):

See this file.

view this post on Zulip Yury G. Kudryashov (Aug 21 2020 at 22:31):

Notations using {} are defined in c++

view this post on Zulip Alex J. Best (Aug 21 2020 at 22:31):

It is, you can do set_option pp.notation false then #check to see what it is though. I linked to a location in the c code where some of this is handled in another thread a week ago looks like Bryan beat me!

view this post on Zulip Bryan Gin-ge Chen (Aug 21 2020 at 22:32):

I copied the link from your message :smiley:


Last updated: May 08 2021 at 10:12 UTC