Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
type th_def = {
sorts : (string
* ((int * int)
* (string ->
(Smtlib_ty.ty list * int list) ->
Smtlib_ty.desc)))
list;
funs : (string * Smtlib_typed_env.fun_def) list;
par_funs : (string * (string list -> Smtlib_typed_env.fun_def)) list;
}
val new_fun :
Smtlib_ty.ty list ->
Smtlib_ty.ty ->
Smtlib_typed_env.assoc option ->
Smtlib_typed_env.fun_def
val core : th_def
val ints : th_def
val reals : th_def
val reals_ints : th_def
val arrays : th_def
val floating_point : th_def
val bit_vectors : th_def
val add_theories : Smtlib_typed_env.env -> theory list -> Smtlib_typed_env.env
val set_logic :
Smtlib_typed_env.env ->
string Smtlib_syntax.data ->
Smtlib_typed_env.env