Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
DeclareSort()
BoolSort()
Const()
Consts()
Eq()
Exists()
ForAll()
FuncRef
Function()
IntSort()
RealSort()
arg()
codomain()
decl()
domains()
eq()
expr_kind()
func_kind()
get_id()
is_accessor()
is_app()
is_constructor()
is_func()
is_if()
is_neg()
is_power()
is_recognizer()
is_uninterp()
is_wf()
num_args()
register_well_formed()
sort()
sort_kind()
Declare a sort with the given name. >>> DeclareSort(“MySort”) MySort