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