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
Theories and Namespaces
Env
Environments
Task
Proof Tasks, Cloning and Meta History
Whyconf
Managing the configuration of Why3
Call_provers
Call provers and parse their outputs
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