Definition of {a,b}

Stream: new members

[Thomas Browning]

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

[Reid Barton]

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

[Reid Barton]

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

[Thomas Browning]

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

[Bryan Gin-ge Chen]

See this file.

[Yury G. Kudryashov]

Notations using {} are defined in c++

[Alex J. Best]

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!

[Bryan Gin-ge Chen]

I copied the link from your message :smiley: