package why3

  1. Overview
  2. Docs
package why3
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 proxy_attr : attribute
val model_projected_attr : attribute
val model_vc_post_attr : attribute
val has_a_model_attr : ident -> bool
val relevant_for_counterexample : ident -> bool
val create_written_attr : Loc.position -> attribute
val extract_written_loc : attribute -> Loc.position option
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 : name:string -> attrs:Sattr.t -> string
val compute_model_trace_field : ident option -> int -> Sattr.t
val extract_field : attribute -> (int * string) option
val get_model_trace_attr : attrs:Sattr.t -> attribute
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