-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Overloading.20infixes.3F
import Mathlib.Tactic.Common
import Mathlib.Mathport.Notation

notation3:70 x " ⊗₁ " y => x * y
infix:70 " ⊗₂ " => Mul.mul

variable (Φ : Type) [Mul Φ] (φ ψ : Φ)

info: φ ⊗₁ ψ : Φ

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: φ ⊗₁ ψ : Φ in #check
φ ⊗₁ ψ : Φ 
φ: Φ
φ ⊗₁ 
ψ: Φ
ψ

info: φ ⊗₂ ψ : Φ

#guard_msgs
Error: ❌ Docstring on `#guard_msgs` does not match generated message:

info: φ ⊗₂ ψ : Φ in #check
φ ⊗₂ ψ : Φ 
φ: Φ
φ ⊗₂ 
ψ: Φ
ψ