Zulip Chat Archive

Stream: general

Topic: rintros


view this post on Zulip Reid Barton (Oct 21 2020 at 01:30):

I'm finding it very convenient to be able to write things like rintro (s : set X) to simultaneously intro and change a hypothesis. How hard would it be to support the syntax rintros (s₀ s₁ : set X)?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:34):

It's actually a bit of coincidence that the notation works out the same as a lambda binder, because it is parsed completely differently

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:35):

in particular, s : set X there is a rcases pattern, so it's not clear whether this entails adding s₀ s₁ : set X as an rcases pattern as well

view this post on Zulip Reid Barton (Oct 21 2020 at 01:35):

oh I see, hmm

view this post on Zulip Reid Barton (Oct 21 2020 at 01:35):

Right, it makes sense at top level like this but in general the (x : t) form makes sense nested inside other patterns as well...

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:36):

I mean we could have a special rintro parser to do this trick only at the top level, or we could do some more extension of rcases_many to allow interpreting pat1 pat2 pat3 as a synonym for <pat1, pat2, pat3>

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:37):

which, oddly enough, might even unify rcases with syntax with cases with

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:41):

although if the default behavior of as_tuple is to transform (<p1, p2, p3> : t) into [(p1:t), (p2:t), (p3:t)] then that could break applications where you actually wanted[(<p1, p2, p3> : t)]. You could fix this with more brackets but it would be a breaking change

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:45):

actually I don't think they can be treated as synonyms, it will break uses like rintro (<x, y> : t) z to look like rintro (x : t) (y : t) z

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:46):

or even just rintro <x, y> z -> rintro x y z which is the most common use case

view this post on Zulip Reid Barton (Oct 21 2020 at 01:50):

Right, it would be nice to unify rcases and cases, but I think the translation would have to be <x y z> as a synonym for <x, y, z>, or <(x y z : int)> for <x : int, y : int, z : int>

view this post on Zulip Reid Barton (Oct 21 2020 at 01:50):

and that feels pretty weird (as well as not matching cases)

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:57):

It wouldn't really be unifying with cases in any case since cases uses unstructured names

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:58):

in the simple structure-destructuring case it might work though

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:59):

question: should rintro ((x y : t) z w : u) be allowed to work and intro 4 things?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 01:59):

it sort of naturally falls out of the grammar I'm writing but it is admittedly a little weird

view this post on Zulip Reid Barton (Oct 21 2020 at 02:05):

So it would mean rintro (x y : t) (z w : u)?

view this post on Zulip Reid Barton (Oct 21 2020 at 02:06):

It seems pretty weird, but on the other hand nobody would have ever tried writing it if you hadn't mentioned it so it wouldn't matter :upside_down:

view this post on Zulip Mario Carneiro (Oct 21 2020 at 02:21):

It would mean rintro ((x : t) : u) ((y : t) : u) (z : u) (w : u)

view this post on Zulip Mario Carneiro (Oct 21 2020 at 02:22):

so that's using change twice at two different types

view this post on Zulip Reid Barton (Oct 21 2020 at 02:22):

Oh... I'm not sure if that's more weird or less weird. I guess less weird?

view this post on Zulip Mario Carneiro (Oct 21 2020 at 02:23):

I will file this under "not my problem if you want to be weird" then

view this post on Zulip Mario Carneiro (Oct 21 2020 at 02:51):

#4722

view this post on Zulip Mario Carneiro (Oct 21 2020 at 02:52):

I didn't implement <x y z> though

view this post on Zulip Mario Carneiro (Oct 21 2020 at 03:31):

Another "so you want to be weird, eh?" is rintro (: t) x which could conceivably mean the same as rintro x. I'm explicitly flagging this one as a parse error though

view this post on Zulip Mario Carneiro (Oct 21 2020 at 06:24):

Hm, it occurs to me that with a simple switching of top level parser, we can also make rintro x y : t work (and mean rintro (x : t) (y : t)). Is that something people want?

view this post on Zulip Floris van Doorn (Oct 21 2020 at 06:51):

That looks pretty nice

view this post on Zulip Mario Carneiro (Oct 21 2020 at 06:56):

oof, another special case: I tried this, and it means that rintro, or rintro : t, are parse errors (instead of no-ops). Good? Bad?

view this post on Zulip Johan Commelin (Oct 21 2020 at 07:07):

Sounds fine to me


Last updated: May 15 2021 at 23:13 UTC