quot_precheck for setBuilder

Stream: mathlib4

[Yakov Pechersky]

I'd like to have a local notation for the set of zero divisors of a ring. My attempt:

import Mathlib

variable {R : Type*} [Mul R] [Zero R]

local notation "ZD" => ({x : R | ∃ (y : R) (_ : y ≠ 0), y * x = 0} : Set R)

but it fails with

no macro or `[quot_precheck]` instance for syntax kind 'Mathlib.Meta.setBuilder' found
  {x : R | ∃ (y : R) (_ : y ≠ 0), y * x = 0}
This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check.

If I follow the suggestion, then the identifier is not registered:

import Mathlib

variable {R : Type*} [Mul R] [Zero R]

set_option quotPrecheck false in
local notation "ZD" => ({x : R | ∃ (y : R) (_ : y ≠ 0), y * x = 0} : Set R)

#check ZD -- unknown identifer 'ZD'

[Yakov Pechersky]

The only example of precheck definition in mathlib I could find is for finset%. I tried defining something similar (cargo culting), but it didn't work:

open Lean.Elab.Term.Quotation in
@[quot_precheck setBuilder] def precheckSetStx : Precheck
  | t@`({ $_:ident | $_ }) => precheck t
  | t@`({ $x:ident : $t | $p }) => precheck t
  | t@`({ $x:ident $b:binderPred | $p }) => precheck t
  | _ => Lean.Elab.throwUnsupportedSyntax

[Kyle Miller]

You could try local notation3 instead

[Kyle Miller]

It appears to work, and it pretty prints.