## Stream: PR reviews

### Topic: lean#402: set builder notation

#### Gabriel Ebner (Jul 22 2020 at 12:57):

I like it and and would be fine with merging it, but I haven't been following the discussion. Is this what people want?
@Kevin Buzzard requested this AFAICT.

#### Johan Commelin (Jul 22 2020 at 13:07):

Since p : X \times Y is not defeq to (p.1, p.2), can we make

{(x, y) | (x y : ℕ) (h : x + y < 10)}


syntactic sugar for

{p | (p : ℕ \times ℕ) (h : p.1 + p.2 < 10)}


because the latter has better defeq behaviour...

#### Anne Baanen (Jul 22 2020 at 13:24):

Making the comma have special behaviour should be possible and in fact it is already a special case in the parser. The rewriting of x to p.1 and y to p.2 is more complicated though, and it would get even worse if we also want to support {(x, (y, z), w) | ...} : set (nat × (nat × nat) × nat)

#### Johan Commelin (Jul 22 2020 at 13:28):

Aha... (maybe it's easier to make p be defeq to (p.1, p.2) :oops: )

#### Kevin Buzzard (Jul 22 2020 at 15:15):

Why would it get worse? rintro can do it?

#### Johan Commelin (Jul 22 2020 at 15:17):

We've had lots of trouble with such definitions right? Wasn't uncurry broken (maybe it still is?)

#### Johan Commelin (Jul 22 2020 at 15:18):

It means you can't apply your predicate to a pair that is not of the form (x,y) and hope that it works. You'll have to manually do cases all the time.

#### Anne Baanen (Jul 22 2020 at 15:30):

I mean the rewriting in the parser would be difficult to implement correctly. The outcome would be easier to use indeed.

#### Rob Lewis (Jul 28 2020 at 15:32):

This is causing trouble here. The changes are all fixable but the fixes feel like regressions. I'm wondering if we should reconsider the syntax here.

#### Mario Carneiro (Jul 28 2020 at 15:35):

Why is {(a, b)} not working anymore?

lean#415

#### Anne Baanen (Jul 28 2020 at 21:09):

Oops, I should have realized this.

#### Anne Baanen (Jul 28 2020 at 21:40):

A quick fix (the syntax of the code is correct but otherwise untested) is to change the lines changed in #415 into the following instead:

        if (p.curr_is_token(get_bar_tk())) {
return parse_set_replacement(p, pos, e);
} else if (p.curr_is_token(get_comma_tk()) || p.curr_is_token(get_rcurly_tk())) {
return parse_fin_set(p, pos, p.patexpr_to_expr(e));
} else {
return p.parser_error_or_expr({"invalid '{' expression, ',', '}', or | expected", p.pos()});
}


We need to accept a , as well as a } to parse it as a singleton + insert (as in lines 247 onwards) fixing lean#418. We also need to call patexpr_to_expr to ensure all variables are bound (because the syntax has binders after the expression, we cannot put anything in scope until we have reached the closing bracket).

#### Anne Baanen (Jul 28 2020 at 21:43):

I assume calling patexpr_to_expr will fix lean#419, although I would have expected the error to look more like "unbound variable α".

#### Gabriel Ebner (Jul 29 2020 at 08:26):

Thanks @Anne Baanen! lean#419

Last updated: May 07 2021 at 17:36 UTC