Lean4
/-- `{ f x y | (x : X) (y : Y) }` is notation for the set of elements `f x y` constructed from the
binders `x` and `y`, equivalent to `{z : Z | ∃ x y, f x y = z}`.
If `f x y` is a single identifier, it must be parenthesized to avoid ambiguity with `{x | p x}`;
for instance, `{(x) | (x : Nat) (y : Nat) (_hxy : x = y^2)}`.
-/
@[term_parser 100]
public meta def «term{_|_}» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Meta.«term{_|_}» 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "{") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ " | "))
Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ "}"))
