class documentation

Undocumented

Method __init__ No summary

Inherited from BaseProverCommand:

Method decorate_proof Modify and return the proof string :param proof_string: str the proof to decorate :param simplify: bool simplify the proof? :return: str
Method get_prover Return the prover object :return: Prover
Method proof Return the proof string :param simplify: bool simplify the proof? :return: str
Method prove Perform the actual proof. Store the result to prevent unnecessary re-proving.
Instance Variable _proof Undocumented
Instance Variable _prover The theorem tool to execute with the assumptions
Instance Variable _result A holder for the result, to prevent unnecessary re-proving

Inherited from BaseTheoremToolCommand (via BaseProverCommand):

Method add_assumptions Add new assumptions to the assumption list.
Method assumptions List the current assumptions.
Method goal Return the goal
Method print_assumptions Print the list of the current assumptions.
Method retract_assumptions Retract assumptions from the assumption list.
Instance Variable _assumptions Undocumented
Instance Variable _goal Undocumented
def __init__(self, goal=None, assumptions=None, prover=None): (source) ΒΆ
Parameters
goal:sem.ExpressionInput expression to prove
assumptions:list(sem.Expression)Input expressions to use as assumptions in the proof.
proverUndocumented