applyto(other) |
|
constants() |
Return a set of individual constants (non-predicates). |
equiv(other[, prover]) |
Check for logical equivalence. |
findtype(variable) |
Find the type of the given variable as it is used in this expression. |
free() |
Return a set of all the free (non-bound) variables. |
fromstring(s[, type_check, signature]) |
|
make_VariableExpression(variable) |
|
negate() |
If this is a negated expression, remove the negation. |
normalize([newvars]) |
Rename auto-generated unique variables |
predicates() |
Return a set of predicates (constants, not variables). |
replace(variable, expression[, ...]) |
Replace every instance of ‘variable’ with ‘expression’ |
simplify() |
| return: | beta-converted version of this expression |
|---|
|
substitute_bindings(bindings) |
|
typecheck([signature]) |
Infer and check types. |
unicode_repr() |
|
variables() |
Return a set of all the variables for binding substitution. |
visit(function, combinator) |
Recursively visit subexpressions. |
visit_structured(function, combinator) |
Recursively visit subexpressions. |