Index of modules

A
Ansi [Pp]
Args [Whyconf]
Args [Debug]

Command line arguments

Args_wrapper

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

B
BigInt

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

C
Call_provers
Coercion
Controller_itp

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

D
Debug

Debug flag handling

Decl

Logic Declarations

DeclTF [Decl]
Driver

Managing the drivers for external provers

E
Env

Environments

Expr
Exthtbl

Association tables over hashable types

Extmap

Association tables over ordered types

Extset

Sets over ordered types

H
H [Wstdlib.MakeMSHW]
H [Wstdlib.MakeMSH]
Hdecl [Decl]
Hfloat [Wstdlib]
Hid [Ident]
Hint [Wstdlib]
Hits [Ity]
Hity [Ity]
Hls [Term]
Hmeta [Theory]
Hpan [Session_itp]
Hpn [Session_itp]
Hpr [Decl]
Hprover [Whyconf]
Hpv [Ity]
Hreg [Ity]
Hrs [Expr]
Hstr [Wstdlib]
Htdecl [Theory]
Hterm [Term]
Hterm_nt_na [Term]
Htn [Session_itp]
Hts [Ty]
Htv [Ty]
Hty [Ty]
Hvs [Term]
I
Ident

Identifiers

Itp_communication
Itp_server

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

Ity
L
Lists

Useful list combinators

Loc

Source locations

M
M [Wstdlib.MakeMSHW]
M [Wstdlib.MakeMSH]
M [Extset.S]

The module of association tables over elt.

Make [Itp_server]
Make [Controller_itp]
Make [Weakhtbl]
Make [Exthtbl]
Make [Extset]

Functor building an implementation of the set structure given a totally ordered type.

Make [Extmap]

Functor building an implementation of the map structure given a totally ordered type.

MakeMSH [Wstdlib]
MakeMSHW [Wstdlib]
MakeOfMap [Extset]

Functor building an implementation of the set structure given a totally ordered type.

Mattr [Ident]
Mdecl [Decl]
Meditor [Whyconf]
Mfloat [Wstdlib]
Mid [Ident]
Mint [Wstdlib]
Mits [Ity]
Mity [Ity]
Mls [Term]
Mmeta [Theory]
Mpr [Decl]
Mprover [Whyconf]
Mpv [Ity]
Mreg [Ity]
Mrs [Expr]
Mstr [Wstdlib]
Mtdecl [Theory]
Mterm [Term]
Mts [Ty]
Mtv [Ty]
Mty [Ty]
Mvs [Term]
Mxs [Ity]
N
Number
O
Opt

Useful option combinators

OrderedHashed [Wstdlib]
OrderedHashedList [Wstdlib]
P
Pdecl
Pmodule
Pp

Helpers for formatted pretty-printing

Pretty

Pretty-printing various objects from Why3's core logic

Printer
Prover [Whyconf]

Printer for prover

R
Rc

Rc file management

S
S [Wstdlib.MakeMSHW]
S [Wstdlib.MakeMSH]
Sattr [Ident]
Sdecl [Decl]
Session_itp

Proof sessions

Sfloat [Wstdlib]
Sid [Ident]
Sint [Wstdlib]
Sits [Ity]
Sity [Ity]
Sls [Term]
Smeta [Theory]
Spr [Decl]
Sprover [Whyconf]
Spv [Ity]
Sreg [Ity]
Srs [Expr]
Sstr [Wstdlib]
Stats [Debug]
Stdecl [Theory]
Sterm [Term]
Strings

Additional Useful Functions on Character Strings

Sts [Ty]
Stv [Ty]
Sty [Ty]
Svs [Term]
Sxs [Ity]
T
Task

Proof Tasks, Cloning and Meta History

Term

Terms and Formulas

TermTF [Term]
Theory
Trans

Task transformations

Ty

Types

U
Util

Useful functions

V
Vc
W
W [Wstdlib.MakeMSHW]
Wdecl [Decl]
Weakhtbl

Hashtables with weak key used for memoization

Wenv [Env]
Whyconf

Managing the configuration of Why3

Wid [Ident]
Wits [Ity]
Wity [Ity]
Wls [Term]
Wpr [Decl]
Wpv [Ity]
Wreg [Ity]
Wrs [Expr]
Wstdlib

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

Wts [Ty]
Wty [Ty]
Wvs [Term]