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

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.

def Std.ExtendedBinder.extBinderParenthesized : Lean.ParserDescr

A extended binder in parentheses

Equations

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

def Std.ExtendedBinder.extBinderCollection : Lean.ParserDescr

A list of parenthesized binders

Equations

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

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.

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

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

Equations

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

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

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

Equations

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

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.

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.