def Lean.binderPred.quot : ParserDescr

def Lean.Parser.Category.binderPred : Category

The syntax category of binder predicates contains predicates like > 0, ∈ s, etc. (: t should not be a binder predicate because it would clash with the built-in syntax for ∀/∃.)

def Lean.«termSatisfies_binder_pred%__» : ParserDescr

satisfies_binder_pred% t pred expands to a proposition expressing that t satisfies pred.

def Lean.«term∃__,_» : ParserDescr

The notation ∃ x < 2, p x is shorthand for ∃ x, x < 2 ∧ p x, and similarly for other binary operators.

def Lean.«term∀__,_» : ParserDescr

The notation ∀ x < 2, p x is shorthand for ∀ x, x < 2 → p x, and similarly for other binary operators.

def Lean.«binderTerm>_» : ParserDescr

Declare ∃ x > y, ... as syntax for ∃ x, x > y ∧ ...

def Lean.«binderTerm≥_» : ParserDescr

Declare ∃ x ≥ y, ... as syntax for ∃ x, x ≥ y ∧ ...

def Lean.«binderTerm<_» : ParserDescr

Declare ∃ x < y, ... as syntax for ∃ x, x < y ∧ ...

def Lean.«binderTerm≤_» : ParserDescr

Declare ∃ x ≤ y, ... as syntax for ∃ x, x ≤ y ∧ ...

def Lean.«binderTerm≠_» : ParserDescr

Declare ∃ x ≠ y, ... as syntax for ∃ x, x ≠ y ∧ ...

def Lean.«binderTerm∈_» : ParserDescr

Declare ∀ x ∈ y, ... as syntax for ∀ x, x ∈ y → ... and ∃ x ∈ y, ... as syntax for ∃ x, x ∈ y ∧ ...

def Lean.«binderTerm∉_» : ParserDescr

Declare ∀ x ∉ y, ... as syntax for ∀ x, x ∉ y → ... and ∃ x ∉ y, ... as syntax for ∃ x, x ∉ y ∧ ...

def Lean.«binderTerm⊆_» : ParserDescr

Declare ∀ x ⊆ y, ... as syntax for ∀ x, x ⊆ y → ... and ∃ x ⊆ y, ... as syntax for ∃ x, x ⊆ y ∧ ...

def Lean.«binderTerm⊂_» : ParserDescr

Declare ∀ x ⊂ y, ... as syntax for ∀ x, x ⊂ y → ... and ∃ x ⊂ y, ... as syntax for ∃ x, x ⊂ y ∧ ...

def Lean.«binderTerm⊇_» : ParserDescr

Declare ∀ x ⊇ y, ... as syntax for ∀ x, x ⊇ y → ... and ∃ x ⊇ y, ... as syntax for ∃ x, x ⊇ y ∧ ...

def Lean.«binderTerm⊃_» : ParserDescr

Declare ∀ x ⊃ y, ... as syntax for ∀ x, x ⊃ y → ... and ∃ x ⊃ y, ... as syntax for ∃ x, x ⊃ y ∧ ...