Documentation

Std.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
  • One or more equations did not get rendered due to their size.
Instances For

    A extended binder in parentheses

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

      A list of parenthesized binders

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

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

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

          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.
          Instances For

            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.
            Instances For

              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.
              Instances For

                Missing docs handler for binder_predicate

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