Lean4
/-- * `{ pat : X | p }` is notation for pattern matching in set-builder notation,
where `pat` is a pattern that is matched by all objects of type `X`
and `p` is a proposition that can refer to variables in the pattern.
It is the set of all objects of type `X` which, when matched with the pattern `pat`,
make `p` come out true.
* `{ pat | p }` is the same, but in the case when the type `X` can be inferred.
For example, `{ (m, n) : ℕ × ℕ | m * n = 12 }` denotes the set of all ordered pairs of
natural numbers whose product is 12.
Note that if the type ascription is left out and `p` can be interpreted as an extended binder,
then the extended binder interpretation will be used. For example, `{ n + 1 | n < 3 }` will
be interpreted as `{ x : Nat | ∃ n < 3, n + 1 = x }` rather than using pattern matching.
-/
@[term_parser 99]
public meta def macroPattSetBuilder : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Meta.macroPattSetBuilder 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "{") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ " : "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ " | "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "}"))
