Why3 API documentation

Util

Useful functions

Opt

Useful option combinators

Lists

Useful list combinators

Strings

Additional Useful Functions on Character Strings

Extmap

Association tables over ordered types

Extset

Sets over ordered types

Exthtbl

Association tables over hashable types

Weakhtbl

Hashtables with weak key used for memoization

Stdlib

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

Rc

Rc file management

Debug

Debug flag handling

Ident

Identifiers

Ty

Types

Term

Terms and Formulas

Decl

Logic Declarations

Theory
Env

Environments

Task

Proof Tasks, Cloning and Meta History

Whyconf

Managing the configuration of Why3

Call_provers
Driver

Managing the drivers for external provers

Session

Proof sessions

Session_tools

Generic tools that can be applied on sessions

Session_scheduler

Scheduling operations on sessions and calls to provers

Mlw_ty

Program Types

Mlw_expr

Program Expressions

Mlw_decl

Program Declarations

Mlw_module

Program modules

Mlw_wp

Weakest preconditions