package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type attribute = private {
  1. attr_string : string;
  2. attr_tag : int;
}
module Mattr : sig ... end
module Sattr : sig ... end
val attr_compare : attribute -> attribute -> int
val attr_equal : attribute -> attribute -> bool
val attr_hash : attribute -> int
val create_attribute : string -> attribute
val list_attributes : unit -> string list
type notation =
  1. | SNword of string
  2. | SNinfix of string
  3. | SNtight of string
  4. | SNprefix of string
  5. | SNget of string
  6. | SNset of string
  7. | SNupdate of string
  8. | SNcut of string
  9. | SNlcut of string
  10. | SNrcut of string
val op_infix : string -> string
val op_tight : string -> string
val op_prefix : string -> string
val op_get : string -> string
val op_set : string -> string
val op_update : string -> string
val op_cut : string -> string
val op_lcut : string -> string
val op_rcut : string -> string
val op_equ : string
val op_neq : string
val sn_decode : string -> notation
val print_decoded : Format.formatter -> string -> unit
type ident = private {
  1. id_string : string;
  2. id_attrs : Sattr.t;
  3. id_loc : Loc.position option;
  4. id_tag : Weakhtbl.tag;
}
module Mid : sig ... end
module Sid : sig ... end
module Hid : sig ... end
module Wid : sig ... end
val id_compare : ident -> ident -> int
val id_equal : ident -> ident -> bool
val id_hash : ident -> int
type preid = {
  1. pre_name : string;
  2. pre_attrs : Sattr.t;
  3. pre_loc : Loc.position option;
}
val id_register : preid -> ident
val id_fresh : ?attrs:Sattr.t -> ?loc:Loc.position -> string -> preid
val id_user : ?attrs:Sattr.t -> string -> Loc.position -> preid
val id_attr : ident -> Sattr.t -> preid
val id_clone : ?attrs:Sattr.t -> ident -> preid
val id_derive : ?attrs:Sattr.t -> string -> ident -> preid
val preid_name : preid -> string
type ident_printer
val create_ident_printer : ?sanitizer:(string -> string) -> string list -> ident_printer
val duplicate_ident_printer : ident_printer -> ident_printer
val id_unique : ident_printer -> ?sanitizer:(string -> string) -> ident -> string
val string_unique : ident_printer -> string -> string
val known_id : ident_printer -> ident -> bool
val forget_id : ident_printer -> ident -> unit
val forget_all : ident_printer -> unit
val sanitizer' : (char -> string) -> (char -> string) -> (char -> string) -> string -> string
val sanitizer : (char -> string) -> (char -> string) -> string -> string
val char_to_alpha : char -> string
val char_to_lalpha : char -> string
val char_to_ualpha : char -> string
val char_to_alnum : char -> string
val char_to_lalnum : char -> string
val char_to_alnumus : char -> string
val char_to_lalnumus : char -> string
val id_unique_attr : ident_printer -> ?sanitizer:(string -> string) -> ident -> string
val model_projected_attr : attribute
val model_vc_attr : attribute
val model_vc_post_attr : attribute
val model_vc_havoc_attr : attribute
val has_a_model_attr : ident -> bool
val remove_model_attrs : attrs:Sattr.t -> Sattr.t
val create_model_trace_attr : string -> attribute
val is_model_trace_attr : attribute -> bool
val append_to_model_trace_attr : attrs:Sattr.t -> to_append:string -> Sattr.t
val append_to_model_element_name : attrs:Sattr.t -> to_append:string -> Sattr.t
val get_model_element_name : attrs:Sattr.t -> string
val get_model_trace_string : attrs:Sattr.t -> string
val get_model_trace_attr : attrs:Sattr.t -> attribute
OCaml

Innovation. Community. Security.