notation for set theoretic constructions

Stream: new members

[Eduardo Freire]

Hello, I have the definition def ord_pair (x y : Set) := pair_set (sing x) (pair_set x y) and want to be able to write (a, b) for ord_pair a b, but I'm struggling to understand how to use notation declarations.

It would also be nice to be able to write {x, y, z} for sing x ∪ sing y ∪ sing z , where sing x is the singleton containing x. For this I tried
notation { l:(foldr , (h t, (sing h) ∪ (sing t)) ∅ }) := l copying the definition of the notation for lists, but this conflicts with other notations that use curly brackets. Any suggestions?

[Yaël Dillies]

The {x, y, z} notation comes from docs#has_insert, so you could declare such an instance.

[Yaël Dillies]

There's also docs#has_singleton and docs#has_lawful_singleton that you might want to have a look at.

[Eduardo Freire]

So the instance of insert should be something like

def insert (a s : Set) : Set := s ∪ sing a

instance : has_insert Set Set :=
⟨insert⟩

?

[Yaël Dillies]

I don't know. This is up to you. However note that whatever your definition is, you probably want to do directly

instance : has_insert Set Set := ⟨λ a s, s ∪ sing a⟩

to avoid having two spellings of insert.

[Eduardo Freire]

I see, thank you. Also, did you mean docs#is_lawful_singleton?

[Eduardo Freire]

Do you know which file defines the notation for has_insert ? It seems like the notation {x, y, z} is not working after defining the has_insert instance.

[Yaël Dillies]

It's a file in C++ I think. That's because curly brackets are used everywhere so Lean can't handle them itself.

[Yaël Dillies]

You're probabyl missing a docs#has_emptyc instance.

[Eduardo Freire]

I do have emptyc, has_singleton and is_lawful_singleton instances