Zulip Chat Archive

Stream: PR reviews

Topic: lean#402: set builder notation


view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip Johan Commelin (Jul 22 2020 at 13:28):

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

view this post on Zulip Kevin Buzzard (Jul 22 2020 at 15:15):

Why would it get worse? rintro can do it?

view this post on Zulip 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?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 28 2020 at 15:35):

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

view this post on Zulip Gabriel Ebner (Jul 28 2020 at 15:38):

lean#415

view this post on Zulip Anne Baanen (Jul 28 2020 at 21:09):

Oops, I should have realized this.

view this post on Zulip 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).

view this post on Zulip 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 α".

view this post on Zulip Gabriel Ebner (Jul 29 2020 at 08:26):

Thanks @Anne Baanen! lean#419


Last updated: May 07 2021 at 17:36 UTC