Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
BinaryContext
MemSorts
MemState
SimState
executeBinary()
executeCBranch()
executeLoad()
executePopcount()
executeSignExtend()
executeStore()
executeSubpiece()
executeUnary()
pc_of_addr()
pretty_insn()
pretty_op()
test_pcode()
insn (Instruction)
str