Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
Consts()
BoolSort()
Const()
DeclareSort()
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()
>>> n = Int("n") >>> xs = Consts("x y z", Lambda([n], n >= 0)) >>> [x.assumes for x in xs] [x >= 0, y >= 0, z >= 0]
names (str)
sort (SortRef | FuncRef)
list[ExprRef]