finding notations definitions

Stream: new members

[Pedro Minicz]

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 notationlist. 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]

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]

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]

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]

I would try Lean 4 :-)

[Yakov Pechersky]

There is a docs#has_sep I think

[Yakov Pechersky]

Check out docs#Set.has_sep