## Stream: new members

### Topic: Definition of {a,b}

#### 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?

#### Reid Barton (Aug 21 2020 at 22:21):

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

#### Reid Barton (Aug 21 2020 at 22:22):

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

#### Thomas Browning (Aug 21 2020 at 22:29):

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

#### Yury G. Kudryashov (Aug 21 2020 at 22:31):

Notations using {} are defined in c++

#### 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!