quotPrecheck はマクロ展開の中にマクロがあると偽陽性を出すことがある

-- エラーになる
/-
no macro or `[quot_precheck]` instance for syntax kind 'Lean.Parser.Term.letMVar' found
  failed to pretty print term (use 'set_option pp.rawOnError true' for raw representation)
This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check.
-/
notation s:70 "[" x:70 "↦" n:70 "]" => (fun v => if v = x then n else s v)

-- `if` がマクロだったので偽陽性を出していただけのようだ
notation s:70 "[" x:70 "↦" n:70 "]" => (fun v => ite (v = x) n (s v))

Reproduce the false positive with the two notation examples in the issue, starting from the quotPrecheck error and comparing the if and ite forms. Trace the macro-expansion path involved in quotation prechecking; done means the nested-macro case no longer reports a missing [quot_precheck] instance while the check still handles genuine failures.