Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
symdef()
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()
PartialExpr
PartialFuncDecl
SymUnion
expr2py
expr2py_default()
py2expr()
e (ExprRef)
object