## Stream: general

### Topic: notation gimmick

#### Kevin Buzzard (Jun 02 2018 at 01:27):

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

#### Kevin Buzzard (Jun 02 2018 at 01:27):

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

#### Kevin Buzzard (Jun 02 2018 at 01:28):

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

#### Kevin Buzzard (Jun 02 2018 at 01:28):

you're such a pessimist

#### Kevin Buzzard (Jun 02 2018 at 01:28):

just because it could be another valid variable name

#### Kevin Buzzard (Jun 02 2018 at 01:29):

what about some weird unicode underline that's not valid

#### Mario Carneiro (Jun 02 2018 at 01:31):

This was a proposal on core lean a while back

#### Simon Hudon (Jun 02 2018 at 01:31):

That's a terrible idea.

#### Mario Carneiro (Jun 02 2018 at 01:31):

oh wait I misunderstood

#### Mario Carneiro (Jun 02 2018 at 01:31):

I thought you wanted to avoid the gamma and R decls

#### Kevin Buzzard (Jun 02 2018 at 01:32):

it's the underscore I want

sorry

#### Mario Carneiro (Jun 02 2018 at 01:32):

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 (Jun 02 2018 at 01:32):

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

#### Mario Carneiro (Jun 02 2018 at 01:33):

That's actually been discussed before too

#### Kevin Buzzard (Jun 02 2018 at 01:33):

proper subscript would be brilliant

#### Mario Carneiro (Jun 02 2018 at 01:33):

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

#### Kevin Buzzard (Jun 02 2018 at 01:34):

sometimes I know that

#### Kevin Buzzard (Jun 02 2018 at 01:34):

I have been browsing that file

#### Kevin Buzzard (Jun 02 2018 at 01:34):

I was looking for cool curly sheaf notation :-)

#### Mario Carneiro (Jun 02 2018 at 01:35):

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

#### Simon Hudon (Jun 02 2018 at 01:38):

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 (Jun 02 2018 at 01:54):

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

#### Simon Hudon (Jun 02 2018 at 01:57):

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

Last updated: May 14 2021 at 23:14 UTC