Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c, d, e) => phi(a, b, c, d, e))
.
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c, d) => phi(a, b, c, d))
.
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as
Sort.all((a, b, c) => phi(a, b, c))
.
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as Sort.all((a, b) => phi(a, b))
.
Higher-order syntax for universal quantifiers.
Higher-order syntax for universal quantifiers. This makes it possible
to write a quantifier as Sort.all(a => phi(a))
.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Extract a term representation of some value in the sort.
Extract a term representation of some value in the sort.
Extract terms from a model.
The variable with given de Bruijn index and this
sort.
The variable with given de Bruijn index and this
sort.
The cardinality of sorts with fixed-size, finite domain.
Extract a term representation of some value in the sort.
Higher-order syntax for epsilon-expressions.
Higher-order syntax for epsilon-expressions. This makes it possible
to write things like Sort.eps(a => phi(a))
.
Generate an epsilon-expression.
Generate an epsilon-expression.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c, d, e) => phi(a, b, c, d, e))
.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c, d) => phi(a, b, c, d))
.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as
Sort.ex((a, b, c) => phi(a, b, c))
.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as Sort.ex((a, b) => phi(a, b))
.
Higher-order syntax for existential quantifiers.
Higher-order syntax for existential quantifiers. This makes it possible
to write a quantifier as Sort.ex(a => phi(a))
.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Add an existential quantifier for the variable with de Bruijn index 0, together with a guard representing this sort.
Terms representing elements of the sort.
Constraints defining the range of the sort.
Allocation of a new constant with this
sort.
Allocation of a new constant with this
sort.
A witness term proving that the sort is inhabited.
A witness term proving that the sort is inhabited.
Modulo sorts, representing the interval
[lower, upper]
with wrap-around arithmetic.