Documentation

Init.BinderPredicates

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

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

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

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.

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

Equations

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

Equations

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

Equations

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

Equations

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

Equations

Declare ∀ x ∈ y, ... as syntax for ∀ x, x ∈ y → ... and ∃ x ∈ y, ... as syntax for ∃ x, x ∈ y ∧ ...

Equations

Declare ∀ x ∉ y, ... as syntax for ∀ x, x ∉ y → ... and ∃ x ∉ y, ... as syntax for ∃ x, x ∉ y ∧ ...

Equations

Declare ∀ x ⊆ y, ... as syntax for ∀ x, x ⊆ y → ... and ∃ x ⊆ y, ... as syntax for ∃ x, x ⊆ y ∧ ...

Equations

Declare ∀ x ⊂ y, ... as syntax for ∀ x, x ⊂ y → ... and ∃ x ⊂ y, ... as syntax for ∃ x, x ⊂ y ∧ ...

Equations

Declare ∀ x ⊇ y, ... as syntax for ∀ x, x ⊇ y → ... and ∃ x ⊇ y, ... as syntax for ∃ x, x ⊇ y ∧ ...

Equations

Declare ∀ x ⊃ y, ... as syntax for ∀ x, x ⊃ y → ... and ∃ x ⊃ y, ... as syntax for ∃ x, x ⊃ y ∧ ...

Equations