Stream: general

Topic: local notation for fin (n+1)

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...

hmm

Kevin Buzzard (May 24 2018 at 08:40):

[n] already means something else

Kevin Buzzard (May 24 2018 at 08:40):

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

Kevin Buzzard (May 24 2018 at 08:41):

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

Kevin Buzzard (May 24 2018 at 08:41):

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

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 (-;

Kevin Buzzard (May 24 2018 at 08:58):

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


Kevin Buzzard (May 24 2018 at 08:58):

you just broke list ;-)

at least locally

Kevin Buzzard (May 24 2018 at 08:58):

of course, this might be clever :-)

Kevin Buzzard (May 24 2018 at 08:59):

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

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...

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

Kevin Buzzard (May 24 2018 at 09:16):

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

Patrick Massot (May 24 2018 at 09:16):

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

Kevin Buzzard (May 24 2018 at 09:16):

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

Patrick Massot (May 24 2018 at 09:17):

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

Kevin Buzzard (May 24 2018 at 09:17):

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

Kevin Buzzard (May 24 2018 at 09:17):

I think Lean should just infer which notation is being used

Kevin Buzzard (May 24 2018 at 09:17):

it has an elaborator, right?

Patrick Massot (May 24 2018 at 09:17):

Sometimes it does

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"...

Sean Leather (May 24 2018 at 09:20):

Patrick: Aww, I liked the latter interpretation better.

Kevin Buzzard (May 24 2018 at 09:25):

Man, that would be a pretty crazy Lean 4 development

Kevin Buzzard (May 24 2018 at 09:25):

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

Kevin Buzzard (May 24 2018 at 09:25):

the metamath approach

Patrick Massot (May 24 2018 at 09:26):

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

Sean Leather (May 24 2018 at 09:26):

Slogan: How To Be Lean: Elaborate It Yourself!

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.

Reid Barton (May 24 2018 at 18:18):

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

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.

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

Johan Commelin (May 24 2018 at 18:25):

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

Mario Carneiro (May 24 2018 at 18:25):

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

Mario Carneiro (May 24 2018 at 18:26):

but global notations require global coordination

Johan Commelin (May 24 2018 at 18:26):

Ok, understood

Last updated: May 14 2021 at 14:20 UTC