Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
num_args()
Eq()
arg()
decl()
eq()
expr_kind()
func_kind()
get_id()
is_accessor()
is_app()
is_constructor()
is_if()
is_power()
is_recognizer()
is_uninterp()
sort()
sort_kind()