notation gimmick

Stream: general

[Kevin Buzzard]

If I have a family of rings {gamma : Type} (R : gamma -> Type) [forall i, ring (R i)]

[Kevin Buzzard]

For a mathematician it would look clearer if I could write forall i, ring R_i

[Kevin Buzzard]

can i make R an instance of some notation typeclass or use some other notation gimmick to do this?

[Kenny Lau]

madness

[Kevin Buzzard]

you're such a pessimist

[Kevin Buzzard]

just because it could be another valid variable name

[Kevin Buzzard]

what about some weird unicode underline that's not valid

[Mario Carneiro]

This was a proposal on core lean a while back

[Simon Hudon]

That's a terrible idea.

[Mario Carneiro]

oh wait I misunderstood

[Mario Carneiro]

I thought you wanted to avoid the gamma and R decls

[Kevin Buzzard]

it's the underscore I want

[Kevin Buzzard]

sorry

[Mario Carneiro]

R_i parsed as nonatomic is a terrible idea, underscores are used gratuitously in lean as spaces that don't break the identifier

[Kevin Buzzard]

We would always talk about a family $R_i$ of rings

[Kevin Buzzard]

how about subscript i?

[Mario Carneiro]

That's actually been discussed before too

[Kevin Buzzard]

proper subscript would be brilliant

[Mario Carneiro]

Did you know there is a subscript for every letter except q?

[Kevin Buzzard]

sometimes I know that

[Kevin Buzzard]

I have been browsing that file

[Kevin Buzzard]

I was looking for cool curly sheaf notation :-)

[Mario Carneiro]

Anyway I suggest you don't try too hard to perfectly replicate all the inconsistencies in math notation

[Simon Hudon]

As an additional note, I believe an identifier followed by a subscript (like fooₐ) is treated as one big identifier, not as foo followed by ₐ

[Kevin Buzzard]

Yes I'm sure you're right. It would just look less nerdy

[Simon Hudon]

Hmmm, a mathematician complaining about looking too nerdy ...