Index of modules

A
Args [Whyconf]
Args [Debug]

Command line arguments

B
Base_scheduler [Session_scheduler]

A functor (a state is hidden) that provide a working scheduler and which can be used as base for an OBSERVER

C
Call_provers
D
Debug

Debug flag handling

Decl

Logic Declarations

DeclTF [Decl]
Driver

Managing the drivers for external provers

E
Env

Environments

Exthtbl

Association tables over hashable types

Extmap

Association tables over ordered types

Extset

Sets over ordered types

H
H [Stdlib.MakeMSHW]
H [Stdlib.MakeMSH]
Hdecl [Decl]
Hfloat [Stdlib]
Hid [Ident]
Hint [Stdlib]
Hits [Mlw_ty]
Hity [Mlw_ty]
Hls [Term]
Hmeta [Theory]
Hpr [Decl]
Hprover [Whyconf]
Hps [Mlw_expr]
Hpv [Mlw_ty]
Hreg [Mlw_ty]
Hstr [Stdlib]
Htdecl [Theory]
Hterm [Term]
Hts [Ty]
Htv [Ty]
Hty [Ty]
Hvs [Term]
I
Ident

Identifiers

L
Lists

Useful list combinators

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

The module of association tables over elt.

Make [Session_scheduler]
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 [Stdlib]
MakeMSHW [Stdlib]
MakeOfMap [Extset]

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

Mdecl [Decl]
Meditor [Whyconf]
Mexn [Mlw_ty]
Mfloat [Stdlib]
Mid [Ident]
Mint [Stdlib]
Mits [Mlw_ty]
Mity [Mlw_ty]
Mlab [Ident]
Mls [Term]
Mlw_decl

Program Declarations

Mlw_expr

Program Expressions

Mlw_module

Program modules

Mlw_ty

Program Types

Mlw_wp

Weakest preconditions

Mmeta [Theory]
Mmeta_args [Session]
Mmetas_args [Session]
Mpr [Decl]
Mprover [Whyconf]
Mps [Mlw_expr]
Mpv [Mlw_ty]
Mreg [Mlw_ty]
Mstr [Stdlib]
Mtdecl [Theory]
Mterm [Term]
Mts [Ty]
Mtv [Ty]
Mty [Ty]
Mvs [Term]
O
Opt

Useful option combinators

OrderedHashed [Stdlib]
OrderedHashedList [Stdlib]
P
PHprover [Session]
PHstr [Session]
Prover [Whyconf]

Printer for prover

R
Rc

Rc file management

S
S [Stdlib.MakeMSHW]
S [Stdlib.MakeMSH]
Sdecl [Decl]
Session

Proof sessions

Session_scheduler

Scheduling operations on sessions and calls to provers

Session_tools

Generic tools that can be applied on sessions

Sexn [Mlw_ty]
Sfloat [Stdlib]
Sid [Ident]
Sint [Stdlib]
Sits [Mlw_ty]
Sity [Mlw_ty]
Slab [Ident]
Sls [Term]
Smeta [Theory]
Smeta_args [Session]
Spr [Decl]
Sprover [Whyconf]
Sps [Mlw_expr]
Spv [Mlw_ty]
Sreg [Mlw_ty]
Sstr [Stdlib]
Stats [Debug]
Stdecl [Theory]
Stdlib

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

Sterm [Term]
Strings

Additional Useful Functions on Character Strings

Sts [Ty]
Stv [Ty]
Sty [Ty]
Svs [Term]
T
T [Mlw_ty]
Task

Proof Tasks, Cloning and Meta History

Term

Terms and Formulas

TermTF [Term]
Theory
Todo [Session_scheduler]
Ty

Types

U
Util

Useful functions

W
W [Stdlib.MakeMSHW]
Wdecl [Decl]
Weakhtbl

Hashtables with weak key used for memoization

Wenv [Env]
Whyconf

Managing the configuration of Why3

Wid [Ident]
Wits [Mlw_ty]
Wity [Mlw_ty]
Wls [Term]
Wpr [Decl]
Wps [Mlw_expr]
Wpv [Mlw_ty]
Wreg [Mlw_ty]
Wts [Ty]
Wty [Ty]
Wvs [Term]