Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
BaseSolver
EProverTHFSolver
LeoIIISolver
MultiSolver
NanoCopISolver
SATSolver
TweeSolver
VampireSolver
VampireTHFSolver
ZipperpositionSolver
binpath()
collect_decls()
collect_sorts()
expr_to_smtlib()
expr_to_tptp()
funcdecl_smtlib()
install_solvers()
install_solvers2()
mangle_decl()
mangle_decl_smtlib()
run()
smt2tptp()
smtlib_datatypes()
sort_to_tptp()
tptp2smt()
all_pairs()
basic()
huet()
huet_smt2_file()
is_trivial()
orient()
simplify()
Add two multisets
>>> list(add([("a", 1), ("b", 2)], [("a", 1), ("c", 3)])) [('a', 2), ('b', 2), ('c', 3)]