TransRelUpdater

class proveit.TransRelUpdater(expr, assumptions=None)

Bases: object

Transitive relation updater: A convenient class for updating a transitive relation (equality, less, subset, etc.) by adding relations that modify the relation via transitivity.

Methods Summary

update(self, relation)

Update the internal relation by applying transitivity with the given relation.

Methods Documentation

update(self, relation)

Update the internal relation by applying transitivity with the given relation. Return the new expression that is introduced. For example, if the internal expression is ‘b’ and the internal relation is ‘a < b’ and ‘b < c’ is provided, deduce ‘a < c’ as the new internal relation and return ‘c’ as the new internal expression.