Lean4
/-- Set builder syntax. This can be elaborated to either a `Set` or a `Finset` depending on context.
The elaborators for this syntax are located in:
* `Data.Set.Defs` for the `Set` builder notation elaborator for syntax of the form `{x | p x}`,
`{x : α | p x}`, `{binder x | p x}`.
* `Data.Finset.Basic` for the `Finset` builder notation elaborator for syntax of the form
`{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator for syntax of the form
`{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
* `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator for syntax of the form
`{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.
-/
@[term_parser 1000]
public meta def setBuilder : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Meta.setBuilder 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "{") Batteries.ExtendedBinder.extBinder)
(ParserDescr.symbol✝ " | "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "}"))
