Zulip Chat Archive

Stream: general

Topic: notation gimmick


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

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:27):

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

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

view this post on Zulip Kenny Lau (Jun 02 2018 at 01:28):

madness

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:28):

you're such a pessimist

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:28):

just because it could be another valid variable name

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:29):

what about some weird unicode underline that's not valid

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:31):

This was a proposal on core lean a while back

view this post on Zulip Simon Hudon (Jun 02 2018 at 01:31):

That's a terrible idea.

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:31):

oh wait I misunderstood

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:31):

I thought you wanted to avoid the gamma and R decls

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:32):

it's the underscore I want

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:32):

sorry

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

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:32):

We would always talk about a family RiR_i of rings

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:33):

how about subscript i?

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:33):

That's actually been discussed before too

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:33):

proper subscript would be brilliant

view this post on Zulip Mario Carneiro (Jun 02 2018 at 01:33):

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

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:34):

sometimes I know that

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:34):

I have been browsing that file

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:34):

I was looking for cool curly sheaf notation :-)

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

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

view this post on Zulip Kevin Buzzard (Jun 02 2018 at 01:54):

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

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