package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val arg_extra_expl_prefix : string * Arg.spec * string
val goal_expl_task : root:bool -> Task.task -> Ident.ident * string * Task.task
val search_attrs : (Ident.Sattr.t -> 'a list) -> Term.term -> 'a list
val current_shape_version : int
type shape
type bound_shape
val empty_bound_shape : bound_shape
val empty_shape : shape
type shape_v =
  1. | Old_shape of shape
  2. | Bound_shape of bound_shape
val shape_of_string : version:int -> string -> shape_v
val string_of_shape : shape_v -> string
val t_shape_task : version:int -> expl:string -> Task.task -> shape
val is_bound_shape_version : int -> bool
module Gshape : sig ... end
type checksum
val print_checksum : Format.formatter -> checksum -> unit
val string_of_checksum : checksum -> string
val checksum_of_string : string -> checksum
val equal_checksum : checksum -> checksum -> bool
val dumb_checksum : checksum
val buffer_checksum : Buffer.t -> checksum
val task_checksum : ?version:int -> Task.task -> checksum
module type S = sig ... end
module Pairing (Old : S) (New : S) : sig ... end
OCaml

Innovation. Community. Security.