Documentation

Batteries.Util.ExtendedBinder

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

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

Equations
    Instances For

      A extended binder in parentheses

      Equations
        Instances For

          A list of parenthesized binders

          Equations
            Instances For

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

              Equations
                Instances For

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

                  Equations
                    Instances For

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

                      Equations
                        Instances For