Overriding some global notation

Stream: general

[Shreyas Srinivas]

It seems one can override some notations while not others. For an MWE, see below:

import Mathlib

namespace Playground

set_option hygiene false

infixl:65 " + " => add
infixl:70 " · " => mul
infix:75 " ∘ " => concat

class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c -- works

  mul : α → α → α
  mul_assoc : ∀ a b c : α, (a · b) · c = a · (b · c) -- ambigiuous, mixes up with the use `·` for infix op arguments

  concat : α → α → α
  concat_assoc : ∀ a b c : α, (a ∘ b) ∘ c = a ∘ (b ∘ c) -- again ambiguous. mixes up with function composition symbol

end Playground

Is there a way to override these notations as well?

[Eric Wieser]

infixl:70 (priority := 1001) " · " => mul

[Shreyas Srinivas]

This somehow causes the associativity to be ignored:

import Mathlib

namespace Playground

set_option hygiene false

infixl:65 " + " => add
infixl:70 (priority := 1001) " · " => mul
infixl:75 (priority := 1100) " ∘ " => concat

class MyNewAlgebra (α : Type) where
  add : α → α → α
  add_assoc : ∀ a b c : α, a + (b + c) = (a + b) + c -- works

  mul : α → α → α
  mul_assoc : ∀ a b c : α, a · b · c = a · (b · c) -- ambigiuous. works with brackets around (a \. b)

  concat : α → α → α
  concat_assoc : ∀ a b c : α, (a ∘ b) ∘ c = a ∘ (b ∘ c) -- same as above

end Playground

[Shreyas Srinivas]

Basically I borrowed this notation as is from Init's Notation.lean file