local notation for fin (n+1)

Stream: general

[Johan Commelin]

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

[Kevin Buzzard]

hmm

[Kevin Buzzard]

[n] already means something else

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

you just broke list ;-)

[Kevin Buzzard]

at least locally

[Kevin Buzzard]

of course, this might be clever :-)

[Kevin Buzzard]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I think Lean should just infer which notation is being used

[Kevin Buzzard]

it has an elaborator, right?

[Patrick Massot]

Sometimes it does

[Patrick Massot]

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

[Sean Leather]

Patrick: Aww, I liked the latter interpretation better.

[Kevin Buzzard]

Man, that would be a pretty crazy Lean 4 development

[Kevin Buzzard]

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

[Kevin Buzzard]

the metamath approach

[Patrick Massot]

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

[Sean Leather]

Slogan: How To Be Lean: Elaborate It Yourself!

[Reid Barton]

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]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

but global notations require global coordination

[Johan Commelin]

Ok, understood