local notation in variable

Stream: lean4

[Floris van Doorn]

In the following example, my local notation doesn't work when used in a variable.

variable {n : Nat}
set_option quotPrecheck false
local notation "Fₙ" => {k : Nat // k < n}

example {a : Fₙ} : 0 ≤ a.1 := by apply Nat.zero_le _ -- works

variable {a : Fₙ}

example : 0 ≤ a.1 := by apply Nat.zero_le -- uses `sorry`, since the type of `a` contains `sorry`.

Is this a known issue? Is there a way to work around this?

[Patrick Massot]

It is known. I'm on mobile so I can't search, sorry.

[Floris van Doorn]

After searching slightly more, I indeed found this previous thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Notation.20introduces.20sorry

[Floris van Doorn]

So in summary: a workaround is to use set_option hygiene false.

[Sebastien Gouezel]

Would notation3 work here?

[Floris van Doorn]

notation3 has the same behavior

[Damiano Testa]

By the way Floris, I learned this solution from someone also called Floris. :upside_down: