why3 1.3.1 · OCaml Package

type dty

val dty_fresh : unit -> dty

val dty_of_ty : Ty.ty -> dty

val dty_var : Ty.tvsymbol -> dty

val dty_app : Ty.tysymbol -> dty list -> dty

val dty_match : dty -> Ty.ty -> unit

val dty_unify : dty -> dty -> unit

val dty_int : dty

val dty_real : dty

val dty_bool : dty

val dty_str : dty

val dty_fold : 
  (Ty.tysymbol -> 'a list -> 'a) ->
  (Ty.tvsymbol -> 'a) ->
  (int -> 'a) ->
  dty ->
  'a

type dpattern = private {

}

and dpattern_node =

type dbinop =

type dquant =

type dbinder = Ident.preid option * dty * Loc.position option

type dterm = private {

}

and dterm_node =

exception TermExpected

exception FmlaExpected

exception DuplicateVar of string

exception UnboundVar of string

type denv = dterm_node Wstdlib.Mstr.t

val denv_empty : denv

val denv_add_var : denv -> Ident.preid -> dty -> denv

val denv_add_let : denv -> dterm -> Ident.preid -> denv

val denv_add_quant : denv -> dbinder list -> denv

val denv_add_pat : denv -> dpattern -> dty -> denv

val denv_add_term_pat : denv -> dpattern -> dterm -> denv

val denv_get : denv -> string -> dterm_node

val denv_get_opt : denv -> string -> dterm_node option

val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern

val dterm : Coercion.t -> ?loc:Loc.position -> dterm_node -> dterm

val debug_ignore_unused_var : Debug.flag

val attr_w_unused_var_no : Ident.attribute

val check_used_var : Term.term -> Term.vsymbol -> unit

val term : ?strict:bool -> ?keep_loc:bool -> dterm -> Term.term

val fmla : ?strict:bool -> ?keep_loc:bool -> dterm -> Term.term

package why3