Whence subtype?

Stream: new members

[Ignat Insarov]

I am looking at this code:

lemma exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
| ⟨a, h⟩ := ⟨a, h⟩

— And I cannot figure out whence the notation for subtypes { … // … } comes from. Is it built in?

[Ignat Insarov]

There is this structure — is it what { … // … } stands for?

structure subtype {α : Sort u} (p : α → Prop) :=
(val : α) (property : p val)

[Yaël Dillies]

Yup, exactly.

[Ignat Insarov]

So how do we know that this notation stands for this definition?

[Yaël Dillies]

It would good if it were written in the docs... And I can't find where the notation is defined :confused:

[Anne Baanen]

The parser for all the {}-related syntax in Lean 3 can be found in src/frontends/lean/brackets.cpp

[Mario Carneiro]

It's built in. The reason is because there is a lot of overloading of notations that start with {, and lean's notation command can't handle it