package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vsymbol = private {
  1. vs_name : Ident.ident;
  2. vs_ty : Ty.ty;
}
module Mvs : sig ... end
module Svs : sig ... end
module Hvs : sig ... end
module Wvs : sig ... end
val vs_compare : vsymbol -> vsymbol -> int
val vs_equal : vsymbol -> vsymbol -> bool
val vs_hash : vsymbol -> int
val create_vsymbol : Ident.preid -> Ty.ty -> vsymbol
type lsymbol = private {
  1. ls_name : Ident.ident;
  2. ls_args : Ty.ty list;
  3. ls_value : Ty.ty option;
  4. ls_constr : int;
}
module Mls : sig ... end
module Sls : sig ... end
module Hls : sig ... end
module Wls : sig ... end
val ls_compare : lsymbol -> lsymbol -> int
val ls_equal : lsymbol -> lsymbol -> bool
val ls_hash : lsymbol -> int
val create_lsymbol : ?constr:int -> Ident.preid -> Ty.ty list -> Ty.ty option -> lsymbol
val create_fsymbol : ?constr:int -> Ident.preid -> Ty.ty list -> Ty.ty -> lsymbol
val create_psymbol : Ident.preid -> Ty.ty list -> lsymbol
val ls_ty_freevars : lsymbol -> Ty.Stv.t
exception EmptyCase
exception DuplicateVar of vsymbol
exception UncoveredVar of vsymbol
exception BadArity of lsymbol * int
exception FunctionSymbolExpected of lsymbol
exception PredicateSymbolExpected of lsymbol
exception ConstructorExpected of lsymbol
exception InvalidIntegerLiteralType of Ty.ty
exception InvalidRealLiteralType of Ty.ty
exception InvalidStringLiteralType of Ty.ty
type pattern = private {
  1. pat_node : pattern_node;
  2. pat_vars : Svs.t;
  3. pat_ty : Ty.ty;
}
and pattern_node =
  1. | Pwild
  2. | Pvar of vsymbol
  3. | Papp of lsymbol * pattern list
  4. | Por of pattern * pattern
  5. | Pas of pattern * vsymbol
val pat_wild : Ty.ty -> pattern
val pat_var : vsymbol -> pattern
val pat_app : lsymbol -> pattern list -> Ty.ty -> pattern
val pat_or : pattern -> pattern -> pattern
val pat_as : pattern -> vsymbol -> pattern
val pat_map : (pattern -> pattern) -> pattern -> pattern
val pat_fold : ('a -> pattern -> 'a) -> 'a -> pattern -> 'a
val pat_all : (pattern -> bool) -> pattern -> bool
val pat_any : (pattern -> bool) -> pattern -> bool
type quant =
  1. | Tforall
  2. | Texists
type binop =
  1. | Tand
  2. | Tor
  3. | Timplies
  4. | Tiff
type term = private {
  1. t_node : term_node;
  2. t_ty : Ty.ty option;
  3. t_attrs : Ident.Sattr.t;
  4. t_loc : Loc.position option;
}
and term_node =
  1. | Tvar of vsymbol
  2. | Tconst of Constant.constant
  3. | Tapp of lsymbol * term list
  4. | Tif of term * term * term
  5. | Tlet of term * term_bound
  6. | Tcase of term * term_branch list
  7. | Teps of term_bound
  8. | Tquant of quant * term_quant
  9. | Tbinop of binop * term * term
  10. | Tnot of term
  11. | Ttrue
  12. | Tfalse
and term_bound
and term_branch
and term_quant
and trigger = term list list
val t_equal_strict : term -> term -> bool
val t_compare_strict : term -> term -> int
val t_hash_strict : term -> int
module Mterm_strict : sig ... end
module Sterm_strict : sig ... end
module Hterm_strict : sig ... end
val t_equal : term -> term -> bool
val t_compare : term -> term -> int
val t_hash : term -> int
module Mterm : sig ... end
module Sterm : sig ... end
module Hterm : sig ... end
val t_close_bound : vsymbol -> term -> term_bound
val t_close_branch : pattern -> term -> term_branch
val t_close_quant : vsymbol list -> trigger -> term -> term_quant
val t_open_bound : term_bound -> vsymbol * term
val t_open_branch : term_branch -> pattern * term
val t_open_quant : term_quant -> vsymbol list * trigger * term
val t_open_bound_with : term -> term_bound -> term
val t_clone_bound_id : term_bound -> Ident.preid
val t_open_bound_cb : term_bound -> vsymbol * term * (vsymbol -> term -> term_bound)
val t_open_branch_cb : term_branch -> pattern * term * (pattern -> term -> term_branch)
val t_open_quant_cb : term_quant -> vsymbol list * trigger * term * (vsymbol list -> trigger -> term -> term_quant)
val t_peek_bound : term_bound -> Ident.ident
val t_peek_branch : term_branch -> Ident.Sid.t
val t_peek_quant : term_quant -> Ident.ident list
exception TermExpected of term
exception FmlaExpected of term
val t_type : term -> Ty.ty
val t_prop : term -> term
val t_ty_check : term -> Ty.ty option -> unit
val t_app : lsymbol -> term list -> Ty.ty option -> term
val fs_app : lsymbol -> term list -> Ty.ty -> term
val ps_app : lsymbol -> term list -> term
val t_app_infer : lsymbol -> term list -> term
val ls_arg_inst : lsymbol -> term list -> Ty.ty Ty.Mtv.t
val ls_app_inst : lsymbol -> term list -> Ty.ty option -> Ty.ty Ty.Mtv.t
val check_literal : Constant.constant -> Ty.ty -> unit
val t_var : vsymbol -> term
val t_const : Constant.constant -> Ty.ty -> term
val t_if : term -> term -> term -> term
val t_let : term -> term_bound -> term
val t_case : term -> term_branch list -> term
val t_eps : term_bound -> term
val t_quant : quant -> term_quant -> term
val t_forall : term_quant -> term
val t_exists : term_quant -> term
val t_binary : binop -> term -> term -> term
val t_and : term -> term -> term
val t_or : term -> term -> term
val t_implies : term -> term -> term
val t_iff : term -> term -> term
val t_not : term -> term
val t_true : term
val t_false : term
val t_nat_const : int -> term
val t_int_const : BigInt.t -> term
val t_real_const : ?pow2:BigInt.t -> ?pow5:BigInt.t -> BigInt.t -> term
val t_string_const : string -> term
val stop_split : Ident.attribute
val asym_split : Ident.attribute
val t_and_l : term list -> term
val t_or_l : term list -> term
val t_and_asym : term -> term -> term
val t_or_asym : term -> term -> term
val t_and_asym_l : term list -> term
val t_or_asym_l : term list -> term
val t_let_close : vsymbol -> term -> term -> term
val t_eps_close : vsymbol -> term -> term
val t_case_close : term -> (pattern * term) list -> term
val t_quant_close : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close : vsymbol list -> trigger -> term -> term
val t_exists_close : vsymbol list -> trigger -> term -> term
val t_attr_set : ?loc:Loc.position -> Ident.Sattr.t -> term -> term
val t_attr_add : Ident.attribute -> term -> term
val t_attr_remove : Ident.attribute -> term -> term
val t_attr_copy : term -> term -> term
val t_if_simp : term -> term -> term -> term
val t_let_simp : term -> term_bound -> term
val t_case_simp : term -> term_branch list -> term
val t_quant_simp : quant -> term_quant -> term
val t_forall_simp : term_quant -> term
val t_exists_simp : term_quant -> term
val t_binary_simp : binop -> term -> term -> term
val t_and_simp : term -> term -> term
val t_and_simp_l : term list -> term
val t_or_simp : term -> term -> term
val t_or_simp_l : term list -> term
val t_implies_simp : term -> term -> term
val t_iff_simp : term -> term -> term
val t_not_simp : term -> term
val t_and_asym_simp : term -> term -> term
val t_and_asym_simp_l : term list -> term
val t_or_asym_simp : term -> term -> term
val t_or_asym_simp_l : term list -> term
val t_let_close_simp : vsymbol -> term -> term -> term
val t_case_close_simp : term -> (pattern * term) list -> term
val t_quant_close_simp : quant -> vsymbol list -> trigger -> term -> term
val t_forall_close_simp : vsymbol list -> trigger -> term -> term
val t_exists_close_simp : vsymbol list -> trigger -> term -> term
val t_forall_close_merge : vsymbol list -> term -> term
val t_exists_close_merge : vsymbol list -> term -> term
val ps_equ : lsymbol
val t_equ : term -> term -> term
val t_neq : term -> term -> term
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
val fs_bool_true : lsymbol
val fs_bool_false : lsymbol
val t_bool_true : term
val t_bool_false : term
val fs_tuple : int -> lsymbol
val t_tuple : term list -> term
val is_fs_tuple : lsymbol -> bool
val is_fs_tuple_id : Ident.ident -> int option
val fs_func_app : lsymbol
val t_func_app : term -> term -> term
val t_pred_app : term -> term -> term
val t_func_app_l : term -> term list -> term
val t_pred_app_l : term -> term list -> term
val t_lambda : vsymbol list -> trigger -> term -> term
val t_open_lambda : term -> vsymbol list * trigger * term
val t_open_lambda_cb : term -> vsymbol list * trigger * term * (vsymbol list -> trigger -> term -> term)
val t_is_lambda : term -> bool
val t_closure : lsymbol -> Ty.ty list -> Ty.ty option -> term
val t_app_partial : lsymbol -> term list -> Ty.ty list -> Ty.ty option -> term
val t_func_app_beta : term -> term -> term
val t_pred_app_beta : term -> term -> term
val t_func_app_beta_l : term -> term list -> term
val t_pred_app_beta_l : term -> term list -> term
val t_map : (term -> term) -> term -> term
val t_fold : ('a -> term -> 'a) -> 'a -> term -> 'a
val t_iter : (term -> unit) -> term -> unit
val t_map_fold : ('a -> term -> 'a * term) -> 'a -> term -> 'a * term
val t_all : (term -> bool) -> term -> bool
val t_any : (term -> bool) -> term -> bool
val t_map_simp : (term -> term) -> term -> term
val t_map_sign : (bool -> term -> term) -> bool -> term -> term
val t_map_cont : ((term -> 'a) -> term -> 'a) -> (term -> 'a) -> term -> 'a
val list_map_cont : (('a -> 'b) -> 'c -> 'b) -> ('a list -> 'b) -> 'c list -> 'b
val tr_equal : trigger -> trigger -> bool
val tr_map : (term -> term) -> trigger -> trigger
val tr_fold : ('a -> term -> 'a) -> 'a -> trigger -> 'a
val tr_map_fold : ('a -> term -> 'a * term) -> 'a -> trigger -> 'a * trigger
module TermTF : sig ... end
val t_v_map : (vsymbol -> term) -> term -> term
val t_v_fold : ('a -> vsymbol -> 'a) -> 'a -> term -> 'a
val t_v_all : (vsymbol -> bool) -> term -> bool
val t_v_any : (vsymbol -> bool) -> term -> bool
val t_v_count : ('a -> vsymbol -> int -> 'a) -> 'a -> term -> 'a
val t_v_occurs : vsymbol -> term -> int
val t_subst_single : vsymbol -> term -> term -> term
val t_subst : term Mvs.t -> term -> term
val t_ty_subst : Ty.ty Ty.Mtv.t -> term Mvs.t -> term -> term
val t_subst_types : Ty.ty Ty.Mtv.t -> term Mvs.t -> term -> term Mvs.t * term
val t_closed : term -> bool
val t_vars : term -> int Mvs.t
val t_freevars : int Mvs.t -> term -> int Mvs.t
val t_ty_freevars : Ty.Stv.t -> term -> Ty.Stv.t
val t_gen_map : (Ty.ty -> Ty.ty) -> (lsymbol -> lsymbol) -> vsymbol Mvs.t -> term -> term
val t_s_map : (Ty.ty -> Ty.ty) -> (lsymbol -> lsymbol) -> term -> term
val t_s_fold : ('a -> Ty.ty -> 'a) -> ('a -> lsymbol -> 'a) -> 'a -> term -> 'a
val t_s_all : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_s_any : (Ty.ty -> bool) -> (lsymbol -> bool) -> term -> bool
val t_ty_map : (Ty.ty -> Ty.ty) -> term -> term
val t_ty_fold : ('a -> Ty.ty -> 'a) -> 'a -> term -> 'a
val t_app_map : (lsymbol -> Ty.ty list -> Ty.ty option -> lsymbol) -> term -> term
val t_app_fold : ('a -> lsymbol -> Ty.ty list -> Ty.ty option -> 'a) -> 'a -> term -> 'a
val t_occurs : term -> term -> bool
val t_replace : term -> term -> term -> term
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct