package why3
val dty_fresh : unit -> dtyval dty_var : Ty.tvsymbol -> dtyval dty_app : Ty.tysymbol -> dty list -> dtyval dty_int : dtyval dty_real : dtyval dty_bool : dtyval dty_str : dtyval dty_fold :
(Ty.tysymbol -> 'a list -> 'a) ->
(Ty.tvsymbol -> 'a) ->
(int -> 'a) ->
dty ->
'atype dpattern = private {dp_node : dpattern_node;dp_dty : dty;dp_vars : dty Wstdlib.Mstr.t;dp_loc : Loc.position option;
}and dpattern_node = | DPwild| DPvar of Ident.preid| DPapp of Term.lsymbol * dpattern list| DPor of dpattern * dpattern| DPas of dpattern * Ident.preid| DPcast of dpattern * dty
type dbinder = Ident.preid option * dty * Loc.position optionand dterm_node = | DTvar of string * dty| DTgvar of Term.vsymbol| DTconst of Constant.constant * dty| DTapp of Term.lsymbol * dterm list| DTfapp of dterm * dterm| DTif of dterm * dterm * dterm| DTlet of dterm * Ident.preid * dterm| DTcase of dterm * (dpattern * dterm) list| DTeps of Ident.preid * dty * dterm| DTquant of dquant * dbinder list * dterm list list * dterm| DTbinop of dbinop * dterm * dterm| DTnot of dterm| DTtrue| DTfalse| DTcast of dterm * dty| DTuloc of dterm * Loc.position| DTattr of dterm * Ident.Sattr.t
type denv = dterm_node Wstdlib.Mstr.tval denv_empty : denvval denv_add_var : denv -> Ident.preid -> dty -> denvval denv_add_let : denv -> dterm -> Ident.preid -> denvval denv_get : denv -> string -> dterm_nodeval denv_get_opt : denv -> string -> dterm_node optionval dpattern : ?loc:Loc.position -> dpattern_node -> dpatternval dterm : Coercion.t -> ?loc:Loc.position -> dterm_node -> dtermval debug_ignore_unused_var : Debug.flagval attr_w_unused_var_no : Ident.attributeval check_used_var : Term.term -> Term.vsymbol -> unit