Lean4
/-- `∃! x : α, p x` means that there exists a unique `x` in `α` such that `p x`.
This is notation for `ExistsUnique (fun (x : α) ↦ p x)`.
This notation does not allow multiple binders like `∃! (x : α) (y : β), p x y`
as a shorthand for `∃! (x : α), ∃! (y : β), p x y` since it is liable to be misunderstood.
Often, the intended meaning is instead `∃! q : α × β, p q.1 q.2`.
-/
@[term_parser 1000]
public meta def «term∃!_,_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Notation.«term∃!_,_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∃!") Lean.explicitBinders)
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
