package why3

  1. Overview
  2. Docs
package why3
Legend:
Library
Module
Module type
Parameter
Class
Class type
type tvsymbol = private {
  1. tv_name : Ident.ident;
}
module Mtv : sig ... end
module Stv : sig ... end
module Htv : sig ... end
val tv_compare : tvsymbol -> tvsymbol -> int
val tv_equal : tvsymbol -> tvsymbol -> bool
val tv_hash : tvsymbol -> int
val create_tvsymbol : Ident.preid -> tvsymbol
val tv_of_string : string -> tvsymbol
type !'a type_def =
  1. | NoDef
  2. | Alias of 'a
  3. | Range of Number.int_range
  4. | Float of Number.float_format
type tysymbol = private {
  1. ts_name : Ident.ident;
  2. ts_args : tvsymbol list;
  3. ts_def : ty type_def;
}
and ty = private {
  1. ty_node : ty_node;
  2. ty_tag : Weakhtbl.tag;
}
and ty_node = private
  1. | Tyvar of tvsymbol
  2. | Tyapp of tysymbol * ty list
module Mts : sig ... end
module Sts : sig ... end
module Hts : sig ... end
module Wts : sig ... end
module Mty : sig ... end
module Sty : sig ... end
module Hty : sig ... end
module Wty : sig ... end
val ts_compare : tysymbol -> tysymbol -> int
val ty_compare : ty -> ty -> int
val ts_equal : tysymbol -> tysymbol -> bool
val ty_equal : ty -> ty -> bool
val ts_hash : tysymbol -> int
val ty_hash : ty -> int
exception BadTypeArity of tysymbol * int
exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVar of tvsymbol
exception IllegalTypeParameters
exception BadFloatSpec
exception EmptyRange
val create_tysymbol : Ident.preid -> tvsymbol list -> ty type_def -> tysymbol
val ty_var : tvsymbol -> ty
val ty_app : tysymbol -> ty list -> ty
val type_def_map : ('a -> 'a) -> 'a type_def -> 'a type_def
val type_def_fold : ('a -> 'b -> 'a) -> 'a -> 'b type_def -> 'a
val is_alias_type_def : 'a type_def -> bool
val is_range_type_def : 'a type_def -> bool
val is_float_type_def : 'a type_def -> bool
val ty_map : (ty -> ty) -> ty -> ty
val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
val ty_all : (ty -> bool) -> ty -> bool
val ty_any : (ty -> bool) -> ty -> bool
val ty_v_map : (tvsymbol -> ty) -> ty -> ty
val ty_v_fold : ('a -> tvsymbol -> 'a) -> 'a -> ty -> 'a
val ty_v_all : (tvsymbol -> bool) -> ty -> bool
val ty_v_any : (tvsymbol -> bool) -> ty -> bool
val ty_s_map : (tysymbol -> tysymbol) -> ty -> ty
val ty_s_fold : ('a -> tysymbol -> 'a) -> 'a -> ty -> 'a
val ty_s_all : (tysymbol -> bool) -> ty -> bool
val ty_s_any : (tysymbol -> bool) -> ty -> bool
exception TypeMismatch of ty * ty
val ty_match : ty Mtv.t -> ty -> ty -> ty Mtv.t
val ts_match_args : tysymbol -> ty list -> ty Mtv.t
val ty_match_args : ty -> ty Mtv.t
val ty_inst : ty Mtv.t -> ty -> ty
val ty_freevars : Stv.t -> ty -> Stv.t
val ty_closed : ty -> bool
val ty_equal_check : ty -> ty -> unit
val ts_int : tysymbol
val ts_real : tysymbol
val ts_bool : tysymbol
val ts_str : tysymbol
val ty_int : ty
val ty_real : ty
val ty_bool : ty
val ty_str : ty
val ts_func : tysymbol
val ty_func : ty -> ty -> ty
val ty_pred : ty -> ty
val ts_tuple : int -> tysymbol
val ty_tuple : ty list -> ty
val is_ts_tuple : tysymbol -> bool
val is_ts_tuple_id : Ident.ident -> int option
exception UnexpectedProp
val oty_compare : ty option -> ty option -> int
val oty_equal : ty option -> ty option -> bool
val oty_hash : ty option -> int
val oty_type : ty option -> ty
val oty_cons : ty list -> ty option -> ty list
val oty_match : ty Mtv.t -> ty option -> ty option -> ty Mtv.t
val oty_inst : ty Mtv.t -> ty option -> ty option
val oty_freevars : Stv.t -> ty option -> Stv.t
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