class documentation

This an abstract class for any Expression that binds a variable in an Expression. This includes LambdaExpressions and Quantified Expressions

Method __eq__ Defines equality modulo alphabetic variance. If we are comparing x.M and y.N, then check equality of M and N[x/y].
Method __init__ No summary
Method __ne__ Undocumented
Method alpha_convert Rename all occurrences of the variable introduced by this variable binder in the expression to newvar. :param newvar: Variable, for the new variable
Method findtype :see Expression.findtype()
Method free No summary
Method replace No summary
Method visit No summary
Method visit_structured No summary
Instance Variable term Undocumented
Instance Variable variable Undocumented

Inherited from Expression:

Class Method fromstring Undocumented
Method __and__ Undocumented
Method __call__ Undocumented
Method __gt__ Undocumented
Method __hash__ Undocumented
Method __lt__ Undocumented
Method __neg__ Undocumented
Method __or__ Undocumented
Method __repr__ Undocumented
Method __str__ Undocumented
Method applyto Undocumented
Method constants Return a set of individual constants (non-predicates). :return: set of Variable objects
Method equiv Check for logical equivalence. Pass the expression (self <-> other) to the theorem prover. If the prover says it is valid, then the self and other are equal.
Method make_VariableExpression Undocumented
Method negate If this is a negated expression, remove the negation. Otherwise add a negation.
Method normalize Rename auto-generated unique variables
Method predicates Return a set of predicates (constants, not variables). :return: set of Variable objects
Method simplify No summary
Method substitute_bindings No summary
Method typecheck Infer and check types. Raise exceptions if necessary.
Method variables Return a set of all the variables for binding substitution. The variables returned include all free (non-bound) individual variables and any variable starting with '?' or '@'. :return: set of Variable objects...
Method _set_type Set the type of this expression to be the given type. Raise type exceptions where applicable.
Class Variable _logic_parser Undocumented
Class Variable _type_checking_logic_parser Undocumented
def __eq__(self, other): (source)

Defines equality modulo alphabetic variance. If we are comparing x.M and y.N, then check equality of M and N[x/y].

def __init__(self, variable, term): (source)
Parameters
variableVariable, for the variable
termExpression, for the term
def __ne__(self, other): (source)

Undocumented

def alpha_convert(self, newvar): (source)

Rename all occurrences of the variable introduced by this variable binder in the expression to newvar. :param newvar: Variable, for the new variable

def findtype(self, variable): (source)

:see Expression.findtype()

def free(self): (source)
See Also
Expression.free()
def replace(self, variable, expression, replace_bound=False, alpha_convert=True): (source)
See Also
Expression.replace()
def visit(self, function, combinator): (source)
See Also
Expression.visit()
def visit_structured(self, function, combinator): (source)
See Also
Expression.visit_structured()

Undocumented

variable = (source)

Undocumented