Local notation

Stream: mathlib4

[Riccardo Brasca]

I am porting file#group_theory/eckmann_hilton which has

local notation a "<" m ">" b => m a b

at the beginning. When I write

variable (distrib : ∀ a b c d, ((a < m₂ > b) <m₁> c <m₂> d) = (a <m₁> c) <m₂> b <m₁> d)

I get an error at the first > b, saying "expected '>'". Using [m] instead of < m > solves the problem, but I don't know why. Should we avoid < in local notation?

[Mario Carneiro]

Isn't that ambiguous?

[Mario Carneiro]

it seems like it would just read m2 > b as a term

[Mario Carneiro]

In lean 3, local notations also have high priority, meaning that you presumably can't use inequalities at all in that file. To get a similar effect in lean 4 you should use local notation (priority := high)

[Mario Carneiro]

testing it, priority := high is not sufficient, but raising the precedence so that m > b is not a legal input for the m in the notation works:

local notation a " <" m:51 "> " b => m a b

variable (m₁ m₂ : α → α → α)
variable (distrib : ∀ a b c d, ((a <m₂> b) <m₁> c <m₂> d) = (a <m₁> c) <m₂> b <m₁> d)

[Riccardo Brasca]

Thanks!

[Riccardo Brasca]

Also, what happened to include and omit?

[Mario Carneiro]

They are hopefully not necessary anymore. I suspect we will eventually find a need for them but lean 4 is much better at doing the right thing by default