Zulip Chat Archive

Stream: general

Topic: local notation for fin (n+1)


view this post on Zulip Johan Commelin (May 24 2018 at 08:38):

How do I make the following work?

local notation ` [n] ` := fin (n+1)

I need this notation a lot, and all the explicit fin (n+1)'s are driving me crazy. Plus all the off-by-one errors that creep into my code...

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:40):

hmm

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:40):

[n] already means something else

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:40):

Oh -- I think that the n in quotes is a literal n

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:41):

so at the very least you'll want ` [ ` n ` ] `

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:41):

but I am not sure how over-riding already-used notation works

view this post on Zulip Johan Commelin (May 24 2018 at 08:45):

Thanks, it is working now. I didn't know about the existing notation; but using local notation I can override it just fine (-;

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:58):

variable (n : )
#check [n] -- list ℕ

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:58):

you just broke list ;-)

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:58):

at least locally

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:58):

of course, this might be clever :-)

view this post on Zulip Kevin Buzzard (May 24 2018 at 08:59):

although given your smiley convention I think I would have recommended ` (-; ` n ` ;-) `

view this post on Zulip Johan Commelin (May 24 2018 at 09:07):

Hmm, but I guess that the local prefix means that I am still safe. I'm not using lists...

view this post on Zulip Patrick Massot (May 24 2018 at 09:16):

Johan, there are plenty of brackets available. See how I use brackets for commutators in https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/support.lean#L115 for instance

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:16):

But [n] is standard in this game, isn't it?

view this post on Zulip Patrick Massot (May 24 2018 at 09:16):

Sure. [a, b] for commutators is also standard

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:16):

CS : "overloading is bad"; Math "but we do it so well!"

view this post on Zulip Patrick Massot (May 24 2018 at 09:17):

But waiting for CS people to change their notation for lists won't help

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:17):

I don't think Johan should even make the notation local

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:17):

I think Lean should just infer which notation is being used

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:17):

it has an elaborator, right?

view this post on Zulip Patrick Massot (May 24 2018 at 09:17):

Sometimes it does

view this post on Zulip Patrick Massot (May 24 2018 at 09:19):

Sean, I meant: "sometimes it infers which notation is being used", not "sometimes it has an elaborator"...

view this post on Zulip Sean Leather (May 24 2018 at 09:20):

Patrick: Aww, I liked the latter interpretation better.

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:25):

Man, that would be a pretty crazy Lean 4 development

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:25):

"we removed the elaborator to encourage users to write better code"

view this post on Zulip Kevin Buzzard (May 24 2018 at 09:25):

the metamath approach

view this post on Zulip Patrick Massot (May 24 2018 at 09:26):

This time we are happy Mario isn't working on Lean 4

view this post on Zulip Sean Leather (May 24 2018 at 09:26):

Slogan: How To Be Lean: Elaborate It Yourself!

view this post on Zulip Reid Barton (May 24 2018 at 18:18):

I wish there was something between notation and local notation, so that modules could export notation without forcing every downstream client to see it.
For example, something like notation which is tied to the current namespace, so that it is only visible when that namespace is open.

view this post on Zulip Reid Barton (May 24 2018 at 18:18):

(I think that exact idea is probably not very good, but something of that flavor.)

view this post on Zulip Mario Carneiro (May 24 2018 at 18:22):

This is exactly how lean 2 notation used to work. Why it changed, I don't know, and I'm not clear on whether to expect this to be different in lean 4.

view this post on Zulip Mario Carneiro (May 24 2018 at 18:24):

I think that lean 3 notation is not handled very well at all, this is why I avoid all notation overloading in mathlib

view this post on Zulip Johan Commelin (May 24 2018 at 18:25):

Hmmm, ok. Does that mean that my local notation for fin (n+1) is dangerous?

view this post on Zulip Mario Carneiro (May 24 2018 at 18:25):

A local notation is fine, assuming you never use lists in that file

view this post on Zulip Mario Carneiro (May 24 2018 at 18:26):

but global notations require global coordination

view this post on Zulip Johan Commelin (May 24 2018 at 18:26):

Ok, understood


Last updated: May 14 2021 at 14:20 UTC