notation shenanigans

Stream: lean4

[Kenny Lau]

import Mathlib.RingTheory.Polynomial.Basic

@[inherit_doc] notation:9000 R "[X]_" n => Polynomial.degreeLT R n
variable {R : Type*} [Semiring R] {m n : ℕ}

#check R[X]_m × R[X]_n   -- application type mismatch // Prod m
#check (R[X]_m) × R[X]_n -- succeeds

I don't understand what's going on; the precedence of [X]_ is 9000, which is higher than × with 35, so why does Lean group m with ×?

[Kevin Buzzard]

mathlib-free:

def Polynomial.degreeLT (R : Type) (n : Nat) : Type := sorry

@[inherit_doc] notation:9000 R "[X]_" n => Polynomial.degreeLT R n
variable {R : Type} {m n : Nat}

#check R[X]_m × R[X]_n
/-
application type mismatch
  Prod m
argument
  m
has type
  Nat : Type
but is expected to have type
  Type ?u.1600 : Type (?u.1600 + 1)
-/
#check (R[X]_m) × R[X]_n -- succeeds

[Edward van de Meent]

a simple fix is to specify that n should have arg precendence or higher

[Edward van de Meent]

i.e. write notation:9000 R "[X]_" n:arg => ...

[Edward van de Meent]

(also once you add the arg i'm not sure if the full rule should have precedence 9000)