# Documentation

Std.Util.ExtendedBinder

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

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 ∀/∃.)

Instances For

satisfies_binder_pred% t pred expands to a proposition expressing that t satisfies pred.

Instances For

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

Instances For

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

Instances For

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

Instances For

A extended binder in parentheses

Instances For

A list of parenthesized binders

Instances For

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

Instances For

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

Instances For

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

Instances For

Declares a binder predicate. For example:

binder_predicate x " > " y:term => ($x >$y)

Instances For

Missing docs handler for binder_predicate

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For