Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
BaseSolver
CVC5Solver
EProverSolver
EProverTHFSolver
LeanSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
collect_sorts()
download()
install_solvers()
install_solvers2()
run()
smt2tptp()
tptp2smt()
diff()
diff_shim()
expand()
factor()
fresh_symbol()
integ_shim()
integrate()
kdify()
limit()
series()
shim_ho()
simplify()
solve()
sum_shim()
summation()
sympify()
sympy_const()
translate_tuple_args()
>>> x = smt.FreshReal("x") >>> sympy_const(x) x!...
e (ExprRef)
Expr