Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
val inst_and_unify :
('a * Smtlib_ty.ty Smtlib_ty.SMap.t) ->
Smtlib_ty.ty Smtlib_ty.IMap.t ->
Smtlib_ty.ty ->
Smtlib_ty.ty ->
(Stdlib.Lexing.position * Stdlib.Lexing.position) option ->
unit
val find_par_ty :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data ->
Smtlib_ty.ty list ->
string list ->
Smtlib_ty.ty
val find_pattern :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data ->
Smtlib_ty.ty list ->
string list ->
bool ->
Smtlib_ty.ty * Smtlib_ty.ty Smtlib_typed_env.SMap.t
val check_if_dummy :
'a Smtlib_syntax.data ->
'a Smtlib_syntax.data list ->
'a Smtlib_syntax.data list
val check_if_escaped : 'a Smtlib_syntax.data list -> unit
val type_cst : Smtlib_syntax.constant -> 'a -> Smtlib_ty.ty
val type_qualidentifier :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_syntax.qualidentifier_aux Smtlib_syntax.data ->
Smtlib_ty.ty list ->
Smtlib_ty.ty
val type_match_case :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list
* int Smtlib_typed_env.SMap.t) ->
Smtlib_ty.ty ->
(Smtlib_syntax.pattern_aux Smtlib_syntax.data
* Smtlib_syntax.term_aux Smtlib_syntax.data) ->
int Smtlib_typed_env.SMap.t ->
Smtlib_ty.ty
* Smtlib_syntax.term_aux Smtlib_syntax.data list
* int Smtlib_typed_env.SMap.t
val type_key_term :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list) ->
Smtlib_syntax.key_term_aux Smtlib_syntax.data ->
Smtlib_syntax.term_aux Smtlib_syntax.data list
val type_term :
(Smtlib_typed_env.env
* Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_syntax.term_aux Smtlib_syntax.data list) ->
Smtlib_syntax.term_aux Smtlib_syntax.data ->
Smtlib_ty.ty * Smtlib_syntax.term_aux Smtlib_syntax.data list
val get_term :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_typed_env.SMap.key Smtlib_syntax.data list ->
Smtlib_syntax.term_aux Smtlib_syntax.data ->
Smtlib_ty.ty
val get_sorted_locals :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
(Smtlib_typed_env.SMap.key Smtlib_syntax.data
* Smtlib_syntax.sort_aux Smtlib_syntax.data)
list ->
Smtlib_ty.ty Smtlib_typed_env.SMap.t
val get_fun_def_locals :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
('a
* Smtlib_typed_env.SMap.key Smtlib_syntax.data list
* (Smtlib_typed_env.SMap.key Smtlib_syntax.data
* Smtlib_syntax.sort_aux Smtlib_syntax.data)
list
* Smtlib_syntax.sort_aux Smtlib_syntax.data) ->
Smtlib_ty.ty Smtlib_typed_env.SMap.t
* Smtlib_ty.ty
* ('a
* Smtlib_syntax.sort_aux Smtlib_syntax.data list
* Smtlib_syntax.sort_aux Smtlib_syntax.data)
val assertion_stack : Smtlib_typed_env.env Stdlib.Stack.t
val type_command :
(Smtlib_typed_env.env * Smtlib_ty.ty Smtlib_typed_env.SMap.t) ->
Smtlib_syntax.command_aux Smtlib_syntax.data ->
Smtlib_typed_env.env
val typing : Smtlib_syntax.command_aux Smtlib_syntax.data list -> unit