Defines an extended binder syntax supporting ∀ ε > 0, ...∀ ε > 0, ... etc.

ink

def Std.ExtendedBinder.binderPred.quot : Lean.ParserDescr

Equations

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

ink

def Lean.Parser.Category.binderPred : Lean.Parser.Category

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

Equations

• Lean.Parser.Category.binderPred = { }

ink

def Std.ExtendedBinder.«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.

ink

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

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

Equations

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

ink

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

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

Equations

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

ink

def Std.ExtendedBinder.extBinder : Lean.ParserDescr

An extended binder has the form x, x : ty, or x pred where pred is a binderPred like < 2.

Equations

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

ink

def Std.ExtendedBinder.extBinderParenthesized : Lean.ParserDescr

A extended binder in parentheses

Equations

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

ink

def Std.ExtendedBinder.extBinderCollection : Lean.ParserDescr

A list of parenthesized binders

Equations

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

ink

def Std.ExtendedBinder.extBinders : Lean.ParserDescr

A single (unparenthesized) binder, or a list of parenthesized binders

Equations

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

ink

def Std.ExtendedBinder.«term∃ᵉ_,_» : Lean.ParserDescr

The syntax ∃ᵉ (x < 2) (y < 3), p x y∃ᵉ (x < 2) (y < 3), p x y is shorthand for ∃ x < 2, ∃ y < 3, p x y∃ x < 2, ∃ y < 3, p x y∃ y < 3, p x y.

Equations

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

ink

def Std.ExtendedBinder.«term∀ᵉ_,_» : Lean.ParserDescr

The syntax ∀ᵉ (x < 2) (y < 3), p x y∀ᵉ (x < 2) (y < 3), p x y is shorthand for ∀ x < 2, ∀ y < 3, p x y∀ x < 2, ∀ y < 3, p x y∀ y < 3, p x y.

Equations

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

ink

def Std.ExtendedBinder.binderPredicate : Lean.ParserDescr

Declares a binder predicate. For example:

binder_predicate x " > " y:term => `($x > $y)

Equations

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

ink

def Std.ExtendedBinder.checkBinderPredicate : Lean.Linter.MissingDocs.SimpleHandler

Missing docs handler for binder_predicate

Equations

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

ink

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

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

Equations

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

ink

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

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

Equations

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

ink

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

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

Equations

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

ink

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

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

Equations

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