# Zulip Chat Archive

## Stream: new members

### Topic: finding notations definitions

#### Pedro Minicz (Jan 03 2022 at 13:15):

I am struggling to find where the set comprehension notation (e.g. `{x | x = x}`

) is defined. I tried using `#print notation {`

and `#print notation |`

, but both searches resulted in other definitions. Set comprehension also doesn't seem to be present in the full `#print notation`

list. I also tried something with `set_option pp.notation false`

and `set_option pp.all true`

but both didn't give me results that help me find where the notation is defined. I want to see how the notation is defined because I want to define something similar.

```
set_option pp.notation false
#check {x | x = x} -- set_of (λ (x : ?M_1), eq x x) : set ?M_1
set_option pp.notation true
set_option pp.all true
#check {x | x = x} -- {x : ?M_1 | x = x} : set.{u_1} ?M_1
set_option pp.notation false
#check {x | x = x} -- @set_of.{u_1} ?M_1 (λ (x : ?M_1), @eq.{u_1+1} ?M_1 x x) : set.{u_1} ?M_1
```

#### Alex J. Best (Jan 03 2022 at 13:19):

Unfortunately the set builder notation is defined in the core of Lean, and the parser written in C rather than Lean itself, so you can't jump to the definition in the same way as for other notations.

You can find the source code here though https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp, but that won't help you write your own Lean version of course!

#### Alex J. Best (Jan 03 2022 at 13:22):

If you say more about the similar thing you want to define it should be possible to get something that works I believe

#### Pedro Minicz (Jan 03 2022 at 13:30):

That is unfortunate.

Given the following definitions:

```
noncomputable theory
axiom Set : Type
axiom mem : Set → Set → Prop
instance : has_mem Set Set := ⟨mem⟩
axiom separation (φ : Set → Prop) (A : Set) : Set
variables (A y : Set) (φ : Set → Prop)
#check separation (λ x, x ≠ y ∧ φ x) A
```

I want to be able to write `separation (λ x, x ≠ y ∧ φ x) A`

as `{x ∈ A : x ≠ y ∧ φ x}`

.

#### Kevin Buzzard (Jan 03 2022 at 14:17):

I would try Lean 4 :-)

#### Yakov Pechersky (Jan 03 2022 at 14:41):

There is a docs#has_sep I think

#### Yakov Pechersky (Jan 03 2022 at 14:42):

Check out docs#Set.has_sep

Last updated: Dec 20 2023 at 11:08 UTC