package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 {
  1. dp_node : dpattern_node;
  2. dp_dty : dty;
  3. dp_vars : dty Wstdlib.Mstr.t;
  4. dp_loc : Loc.position option;
}
and dpattern_node =
  1. | DPwild
  2. | DPvar of Ident.preid
  3. | DPapp of Term.lsymbol * dpattern list
  4. | DPor of dpattern * dpattern
  5. | DPas of dpattern * Ident.preid
  6. | DPcast of dpattern * dty
type dbinop =
  1. | DTand
  2. | DTand_asym
  3. | DTor
  4. | DTor_asym
  5. | DTimplies
  6. | DTiff
  7. | DTby
  8. | DTso
type dquant =
  1. | DTforall
  2. | DTexists
  3. | DTlambda
type dbinder = Ident.preid option * dty * Loc.position option
type dterm = private {
  1. dt_node : dterm_node;
  2. dt_dty : dty option;
  3. dt_loc : Loc.position option;
}
and dterm_node =
  1. | DTvar of string * dty
  2. | DTgvar of Term.vsymbol
  3. | DTconst of Constant.constant * dty
  4. | DTapp of Term.lsymbol * dterm list
  5. | DTfapp of dterm * dterm
  6. | DTif of dterm * dterm * dterm
  7. | DTlet of dterm * Ident.preid * dterm
  8. | DTcase of dterm * (dpattern * dterm) list
  9. | DTeps of Ident.preid * dty * dterm
  10. | DTquant of dquant * dbinder list * dterm list list * dterm
  11. | DTbinop of dbinop * dterm * dterm
  12. | DTnot of dterm
  13. | DTtrue
  14. | DTfalse
  15. | DTcast of dterm * dty
  16. | DTuloc of dterm * Loc.position
  17. | DTattr of dterm * Ident.Sattr.t
exception TermExpected
exception FmlaExpected
exception DuplicateVar of string
exception UnboundVar of string
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
OCaml

Innovation. Community. Security.