Index of modules

A
Ansi [Pp]
Args [Whyconf]
Args [Loc]
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

Call provers and parse their outputs

Check_ce

Validation of candidate counterexamples and classification of proof failures using runtime-assertion checking

Coercion

Support for coercions in the logic language

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

Why3 Environments

Expr

WhyML program expressions

Exthtbl

Association tables over hashable types

Extmap

Association tables over ordered types

Extset

Sets over ordered types

F
F [Ptree_helpers]

Extra helpers for creating declarations in top-down style, functional interface

G
Getopt

Parsing of command-line options

H
H [Wstdlib.MakeMSHW]
H [Wstdlib.MakeMSH]
Hdecl [Decl]
Hfile [Session_itp]
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_strict [Term]
Htn [Session_itp]
Hts [Ty]
Htv [Ty]
Hty [Ty]
Hvs [Term]
I
I [Ptree_helpers]

Extra helpers for creating declarations in top-down style, imperative interface.

Ident

Identifiers

Int [Wstdlib]
Itp_communication

Communication protocol for the ITP server

Itp_server

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

Ity

Types in WhyML programs

L
Lists

Combinators on list type

Loc

Source locations

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

The module of association tables over elt.

Make [Weakhtbl]
Make [Itp_server]
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.

Make [Exthtbl]
Make [Controller_itp]
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]
Mlmpfr_wrapper

Wrapper module for computation on extended floating-point numbers

Mls [Term]
Mlw_printer

Pretty printing of Why3 parse trees as WhyML source code

Mmeta [Theory]
Model_parser

Model

Mpr [Decl]
Mprover [Whyconf]
Mpv [Ity]
Mreg [Ity]
Mrs [Expr]
Mstr [Wstdlib]
Mtdecl [Theory]
Mterm [Term]
Mterm_strict [Term]
Mts [Ty]
Mtv [Ty]
Mty [Ty]
Mv [Pinterp_core]

A map with values as keys

Mvs [Term]
Mxs [Ity]
N
Number

General functions for representations of numeric values

O
Opt

Combinators on option type

OrderedHashed [Wstdlib]
OrderedHashedList [Wstdlib]
P
Pdecl

WhyML program declarations

Pinterp

WhyML Program Interpreter

Pinterp_core

WhyML program interpreter: basic definitions

Pmodule

WhyML program modules

Pp

Helpers for formatted pretty-printing

Pretty
Printer

Task printing

Prover [Whyconf]
Ptree

Parse trees

Ptree_helpers

Helpers for constructing program with the parse tree API

R
Rac

Runtime Assertion Checkers for WhyML programs

Rc

Configuration 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]
Sterm_strict [Term]
Strings

Utility 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

Theories and Namespaces

Trans

Task transformations

Ty

Types

Typing

Typing parse trees

U
Unsafe [Typing]
User [Whyconf]
Util

Various Utility Functions

V
Value [Pinterp_core]

(Mutable) values used in Pinterp

Vc

WhyML VC generators

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

Hashtables with weak key used for memoization

Wenv [Env]
Why [Rac]

RAC implementation using a Why3 transformation and prover

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]