Documentation

Std.Util.ExtendedBinder

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

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

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

    Equations
    Instances For

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

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

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

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

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

            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

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

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

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

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

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

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

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

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

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

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