Local notation priority

Stream: mathlib4

[Yury G. Kudryashov]

How can I make

import Mathlib.Algebra.Abs

variable {α : Type _} {n : ℕ}

set_option quotPrecheck false in
local notation "αⁿ⁺¹" => Fin (n + 1) → α

example : αⁿ⁺¹ := fun _ ↦ const

work? The local notation conflicts with

@[inherit_doc]
postfix:1000 "⁺" => PosPart.pos

from the imported file.

[Yury G. Kudryashov]

I tried local notation:200 and local notation:2000, neither makes it work.

[Floris van Doorn]

that is not the priority but the binding power. Try local notation (priority := high)

[Yury G. Kudryashov]

Doesn't work

[Floris van Doorn]

You misdiagnosed the issue. This works:

import Mathlib.Algebra.Abs

variable {α : Type _} {n : Nat}

set_option quotPrecheck false
local notation "αⁿ⁺¹" => Fin (n + 1) → α

example : αⁿ⁺¹ := sorry

[Floris van Doorn]

You got bitten by this trap: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Notation.20for.20inductive.20types/near/363980933