Psmt2Frontend.Smtlib_typing
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