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
Call provers and parse their outputs

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
Theories and Namespaces
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]