set notation

Stream: general

[Yury G. Kudryashov]

Currently {a, b} is defined as insert b {a}, so various lemmas about insert reverse the order. E.g., Sup {a, b} simplifies to sup b a while I'd expect sup a b. Is there any reason to have it this way?

[Patrick Massot]

From times to times I get random errors using set notations. We can do:

variables s : set ℕ

#check {x | x = 0}
#check {x : ℤ | x = 0}
#check {x ∈ s | x = 0}

But sometimes the second variant rises an error "function expected at", but it's very hard to minimize. Does anyone understand the magic behind this notation? Only the last variation (which is pretty rarely used) has a clear origin using the has_sep class.

[Yury G. Kudryashov]

The first two are parsed in C++ with hardcoded set_of

[Yury G. Kudryashov]

https://github.com/leanprover-community/lean/blob/master/src/frontends/lean/brackets.cpp#L28

[Patrick Massot]

Yes I understand that things that are not defined by Lean code are defined by C++ code. My question was not precise enough. I'd like to know whether other people see random failure with these notations and know how to fix them.

[Mario Carneiro]

I've never seen a failure, but it's possible that it's triggered by certain combinations of leaving things out which I might be systematically avoiding for style reasons