Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
all_smt2()
DeclHole
ExistsHole
ExprCtx
ForAllHole
LambdaHole
QuantifierHole
Zipper
all_values()
alpha_eq()
alpha_norm()
antipattern()
ast_size_sexpr()
bysect()
calling_globals_locals()
consts()
curry_arrays()
decls()
defined_decls()
eunify()
find_calls()
free_in()
free_vars()
generate()
is_strict_subterm()
is_subterm()
is_value()
lambda_lift()
lemma_db()
lift_ite()
occurs()
open_binder()
open_binder_unhygienic()
pathmap()
pmatch()
pmatch_fo()
pmatch_rec()
pmatch_rec_ctx()
prompt()
proofstep_to_smt2()
propagate()
propagate_eqs()
prune()
quant_kind_eq()
sanity_check_consistency()
search_decl()
search_expr()
sorts()
subterms()
unify()
unify_db()
write_smt2_files()