Methods to interpret a theory in a data structure

  • substitute a constant by its value in an expression

  • replace symbols interpreted in a structure by their interpretation

  • expand quantifiers

This module also includes methods to:

  • substitute an node by another in an AST tree

  • instantiate an expresion, i.e. replace a variable by a value

This module monkey-patches the ASTNode class and sub-classes.

( see docs/zettlr/ )

idp_engine.Interpret.add_def_constraints(self, instantiables, problem, result)[source]

result is updated with the constraints for this definition.

The instantiables (of the definition) are expanded in problem.