__init__ ([goal, assumptions, prover]) |
param goal: | Input expression to prove |
|
add_assumptions (new_assumptions) |
Add new assumptions to the assumption list. |
assumptions () |
List the current assumptions. |
decorate_proof (proof_string[, simplify]) |
Modify and return the proof string |
find_answers ([verbose]) |
|
get_prover () |
|
goal () |
Return the goal |
print_assumptions () |
Print the list of the current assumptions. |
proof ([simplify]) |
Return the proof string |
prove ([verbose]) |
Perform the actual proof. |
retract_assumptions (retracted[, debug]) |
Retract assumptions from the assumption list. |