Documentation

Batteries.Util.ExtendedBinder

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

source
def Batteries.ExtendedBinder.extBinder :
Lean.ParserDescr

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

Instances For
    source
    def Batteries.ExtendedBinder.extBinderParenthesized :
    Lean.ParserDescr

    A extended binder in parentheses

    Instances For
      source
      def Batteries.ExtendedBinder.extBinderCollection :
      Lean.ParserDescr

      A list of parenthesized binders

      Instances For
        source
        def Batteries.ExtendedBinder.extBinders :
        Lean.ParserDescr

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

        Instances For
          source
          def Batteries.ExtendedBinder.«term∃ᵉ_,_» :
          Lean.ParserDescr

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

          Instances For
            source
            def Batteries.ExtendedBinder.«term∀ᵉ_,_» :
            Lean.ParserDescr

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

            Instances For