Why3 API documentation

Util

Useful functions

Opt

Useful option combinators

Lists

Useful list combinators

Strings

Additional Useful Functions on Character Strings

Extmap

Association tables over ordered types

Extset

Sets over ordered types

Exthtbl

Association tables over hashable types

Weakhtbl

Hashtables with weak key used for memoization

Wstdlib

Specific instances of Set, Map, Hashtbl on int, string, float, and tagged types

Rc

Rc file management

Debug

Debug flag handling

Loc

Source locations

Pp

Helpers for formatted pretty-printing

BigInt

Wrapper for big nums, implemented either with OCaml's Nums or ZArith

Number
Ident

Identifiers

Ty

Types

Term

Terms and Formulas

Decl

Logic Declarations

Coercion
Theory
Env

Environments

Task

Proof Tasks, Cloning and Meta History

Trans

Task transformations

Pretty

Pretty-printing various objects from Why3's core logic

Printer
Whyconf

Managing the configuration of Why3

Call_provers
Driver

Managing the drivers for external provers

Args_wrapper

Pre-processing of transformations with arguments, including parsing and typing in the context of a task.

Session_itp

Proof sessions

Controller_itp

Controller to run provers and transformations asynchronously on goals of a session

Itp_communication
Itp_server

Server for a client/server communication with an external graphical interface

Ity
Expr
Pdecl
Pmodule
Vc