rintros

Stream: general

[Reid Barton]

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)?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

oh I see, hmm

[Reid Barton]

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

[Mario Carneiro]

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>

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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>

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

in the simple structure-destructuring case it might work though

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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:

[Mario Carneiro]

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

[Mario Carneiro]

so that's using change twice at two different types

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

#4722

[Mario Carneiro]

I didn't implement <x y z> though

[Mario Carneiro]

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

[Mario Carneiro]

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?

[Floris van Doorn]

That looks pretty nice

[Mario Carneiro]

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

[Johan Commelin]

Sounds fine to me