def Lean.binderPred.quot : ParserDescr

Equations

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

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 ∀/∃.)

Equations

• Lean.Parser.Category.binderPred = { }

def Lean.«termSatisfies_binder_pred%__» : 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∃__,_» : 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∀__,_» : 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.«binderPred>_» : ParserDescr

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

Equations

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

def Lean.«binderPred≥_» : ParserDescr

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

Equations

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

def Lean.«binderPred<_» : ParserDescr

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

Equations

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

def Lean.«binderPred≤_» : ParserDescr

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

Equations

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

def Lean.«binderPred≠_» : ParserDescr

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

Equations

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

def Lean.«binderPred∈_» : ParserDescr

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

Equations

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

def Lean.«binderPred∉_» : ParserDescr

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

Equations

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

def Lean.«binderPred⊆_» : ParserDescr

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

Equations

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

def Lean.«binderPred⊂_» : ParserDescr

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

Equations

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

def Lean.«binderPred⊇_» : ParserDescr

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

Equations

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

def Lean.«binderPred⊃_» : ParserDescr

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

Equations

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