def Lean.Parser.Category.binderPred : Lean.Parser.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 ∀/∃.)

Equations

• Lean.Parser.Category.binderPred = { }

def Lean.binderPred.quot : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.«termSatisfies_binder_pred%__» : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

def Lean.«binderTerm>_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm>_» = Lean.ParserDescr.node `Lean.«binderTerm>_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm≥_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm≥_» = Lean.ParserDescr.node `Lean.«binderTerm≥_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm<_» : Lean.ParserDescr

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

def Lean.«binderTerm≤_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm≤_» = Lean.ParserDescr.node `Lean.«binderTerm≤_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm≠_» : Lean.ParserDescr

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

def Lean.«binderTerm∈_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm∈_» = Lean.ParserDescr.node `Lean.«binderTerm∈_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm∉_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm∉_» = Lean.ParserDescr.node `Lean.«binderTerm∉_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∉ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm⊆_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm⊆_» = Lean.ParserDescr.node `Lean.«binderTerm⊆_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm⊂_» : Lean.ParserDescr

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

def Lean.«binderTerm⊇_» : Lean.ParserDescr

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

Equations

• Lean.«binderTerm⊇_» = Lean.ParserDescr.node `Lean.«binderTerm⊇_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊇ ") (Lean.ParserDescr.cat `term 0))

def Lean.«binderTerm⊃_» : Lean.ParserDescr

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