Documentation

Std.Util.ExtendedBinder

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

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

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

Equations

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.

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

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

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

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

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.

A extended binder in parentheses

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

A list of parenthesized binders

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

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

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

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

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

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

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

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.

Missing docs handler for binder_predicate

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

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

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

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

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

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

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

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

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