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 |
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] | |
| HStdecl [Task] | |
| 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 |
| Loc | Source locations |
| Log [Pinterp_core] | |
M | |
| M [Wstdlib.MakeMSHW] | |
| M [Wstdlib.MakeMSH] | |
| M [Extset.S] | The module of association tables over |
| 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. |
| MakeSCC [Wstdlib] | |
| 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 |
| 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 | Pretty-printing various objects from Why3's core logic |
| 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] | |
| Strategy | Proof strategies |
| 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 |
| 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 |
| Wtds [Task] | |
| Wts [Ty] | |
| Wty [Ty] | |
| Wvs [Term] |