-
0B, 6.1
- 0b, 6.1
- 0O, 6.1
- 0o, 6.1
- 0X, 6.1, 6.1, 6.1, 6.1
- 0x, 6.1, 6.1, 6.1, 6.1
- _, 6.1, 6.1, 6.1, 6.1, 6.1, 6.1, 6.3, 6.3, 6.3, 6.3, 6.3, 6.3
- API, 3, 4.1.2
-a , see --apply-transform
- abstract, 6.6.2
- absurd, 6.6.1
--add-prover , 4.2.1, 5.1
- alias, 6.4, 6.4, 6.6.2, 6.6.2
- alias, 6.4, 6.6.2
- alpha, 6.1
- any, 6.4, 6.6.2, 6.6.2
--apply-transform , 5.2
- as, 6.3, 6.5.3, 6.5.3
- assert, 6.6.1
- assertion, 6.6.1
- assume, 6.6.1
- at, 6.3, 6.6.1
- attribute, 6.1
- axiom, 6.5.3
- begin, 6.3, 6.4, 6.4, 6.6.2
- bin-digit, 6.1
- binder, 6.3
- binders, 6.5.2
- bound-var, 6.3
- by, 6.3, 6.5.2
-C , see --config
- Coq proof assistant, 8.3
- check, 6.6.1
- clone, 6.5.3
- coinductive, 6.5.3
compute_in_goal , 9.5.3
compute_specified , 9.5.3
- config, 5.1
--config , 5
- configuration file, 5.1, 8.2.3, 9.3
- constant, 6.5.3
- constant-decl, 6.5.3
-D , see --driver
--debug , 5
--debug-all , 5
- decl, 6.5.3
- detached
--detect-plugins , 5.1
--detect-provers , 5.1
- digit, 6.1
- diverges, 6.4, 6.6.2
- do, 6.6.2, 6.6.2
- done, 6.6.2, 6.6.2
- downto, 6.6.2
--driver , 5.2, 8.2.1
driver , 8.2.3
- driver file, 8.2.2
- Einstein’s logic problem, 2.1
editor_modifiers , 8.2.3
eliminate_algebraic , 9.5.4
eliminate_builtin , 9.5.4
eliminate_definition , 9.5.4
eliminate_definition_func , 9.5.4
eliminate_definition_pred , 9.5.4
eliminate_if , 9.5.4
eliminate_if_fmla , 9.5.4
eliminate_if_term , 9.5.4
eliminate_inductive , 9.5.4
eliminate_let , 9.5.4
eliminate_let_fmla , 9.5.4
eliminate_let_term , 9.5.4
eliminate_mutual_recursion , 9.5.4
eliminate_recursion , 9.5.4
- else, 6.3, 6.4, 6.5.2, 6.6.2, 6.6.2
encoding_smt , 9.5.4
encoding_tptp , 9.5.4
- end, 6.3, 6.3, 6.4, 6.4, 6.4, 6.5.2, 6.5.3, 6.5.3, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.3, 6.6.3
- ensures, 6.4, 6.6.1, 6.6.2
- ensures, 6.6.1
- exception, 6.6.3
- execute, 5.7, 7.1
- exists, 6.3, 6.5.2
- exponent, 6.1
- export, 6.5.3
- expr, 6.4, 6.4, 6.6.2, 6.6.2
- expr-case, 6.6.2
- expr-field, 6.6.2
--extra-config , 5, 8.2.3
- extract, 5.8, 7.2
- extraction, 7.2
- false, 6.3, 6.4, 6.5.2
- file, 6.5.4, 6.6.4
- float, 6.5.3
- for, 6.6.2
- forall, 6.3, 6.5.2
- formula, 6.5.2
- formula-case, 6.5.2
- fun, 6.3, 6.4, 6.6.2, 6.6.2, 6.6.3
- fun-defn, 6.4, 6.6.2
- fun-head, 6.4, 6.6.2
- function, 6.4, 6.5.3, 6.5.3, 6.6.2
- function-decl, 6.5.3
-G , see --goal
- ghost, 6.3, 6.3, 6.3, 6.3, 6.3, 6.4, 6.4, 6.4, 6.4, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.3, 6.6.3, 6.6.3
- goal, 6.5.3, 6.5.3
--goal , 5.2
- h-exponent, 6.1
- handler, 6.6.2
--help , 5
- hex-digit, 6.1
- Isabelle proof assistant, 8.4
- ide, 5.3
- ident-op, 6.3
- if, 6.3, 6.4, 6.5.2, 6.6.2, 6.6.2
- imp-exp, 6.5.3
- import, 6.5.3, 6.5.3, 6.6.3
- in, 6.3, 6.3, 6.4, 6.4, 6.4, 6.5.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2
- ind-case, 6.5.3
induction_ty_lex , 9.5.2
- inductive, 6.5.3
- inductive-decl, 6.5.3
- infix-op-, 6.1, 6.1, 6.1, 6.1
inline_all , 9.5.1
inline_goal , 9.5.1
inline_trivial , 9.5.1
- integer, 6.1
- interpretation
introduce_premises , 9.5.4
- invariant, 6.6.1
- invariant, 6.6.1
- kind, 6.4, 6.6.2
| -L , see --library
- lemma, 6.4, 6.5.3, 6.5.3, 6.6.2
- let, 6.3, 6.3, 6.4, 6.4, 6.4, 6.5.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.3, 6.6.3
- library, 6.7
--library , 5
- lident, 6.1
- lident-ext, 6.3
--list-debug-flags , 5
--list-formats , 5, 5.2
--list-metas , 5
--list-printers , 5
--list-prover-families , 5.1
--list-provers , 1.3, 5, 5.2
--list-transforms , 5, 5.2, 9.5
- logic-decl, 6.5.3
- loop, 6.6.2
- lqualid, 6.1
- match, 6.3, 6.4, 6.5.2, 6.6.2, 6.6.2
- mdecl, 6.6.3
- module, 6.6.3
- module, 6.6.3
- mrecord-field, 6.6.3
- mtype-decl, 6.6.3
- mtype-defn, 6.6.3
- mutable, 6.6.3
- namespace, 6.5.3, 6.5.3, 6.6.3
- not, 6.3, 6.4, 6.5.2
- OCaml, 7.2
- obsolete
- oct-digit, 6.1
- old, 6.3, 6.6.1
- one-variant, 6.6.1
- op-char-, 6.1, 6.1, 6.1, 6.1, 6.1, 6.1, 6.1
option , 8.2.3
-P , see --prover
- PVS proof assistant, 8.5
- param, 6.3
- path, 6.4, 6.6.2
- pattern, 6.3
- pgm-decl, 6.6.3
- pgm-defn, 6.6.3
- plugin, 5.1
- predicate, 6.4, 6.5.3, 6.5.3, 6.6.2
- predicate-decl, 6.5.3
- prefix-op, 6.1
- prove, 5.2
--prover , 5.2
prover_modifiers , 8.2.3
- qident, 6.1
- qualid, 6.3
- qualifier, 6.1
- quant-cast, 6.3
- quant-vars, 6.3
- quantifier, 6.3, 6.5.2
- raise, 6.6.2, 6.6.2
- raises, 6.4, 6.4, 6.6.1, 6.6.1, 6.6.2, 6.6.2
- raises, 6.6.1
- raises-case, 6.6.1
- range, 6.5.3
- reads, 6.4, 6.4, 6.6.1, 6.6.2, 6.6.2
- reads, 6.6.1
- real, 6.1
- realize, 5.9, 8.2.1
realized_theory , 8.2.2
- rec, 6.4, 6.6.2, 6.6.2, 6.6.3
- record-field, 6.5.3
- replay, 5.4
- requires, 6.4, 6.6.1, 6.6.2
- requires, 6.6.1
- result, 6.4, 6.6.2
- ret-name, 6.4, 6.6.2
- ret-type, 6.4, 6.6.2
- returns, 6.4, 6.6.1, 6.6.2
- returns, 6.6.1
simplify_array , 9.5.4
simplify_formula , 9.5.4
simplify_formula_and_task , 9.5.5
simplify_recursive_definition , 9.5.4
simplify_trivial_quantification , 9.5.4
simplify_trivial_quantification_in_goal , 9.5.4
- so, 6.3, 6.5.2
- spec, 6.4, 6.6.1, 6.6.2
split_all , 9.5.5
split_all_full , 9.5.5
split_goal , 9.5.5
split_goal_full , 9.5.5
split_intro , 9.5.5
split_premise , 9.5.4
split_premise_full , 9.5.4
- standard library, 6.7
- subst, 6.5.3
- subst-elt, 6.5.3
- suffix, 6.1
- symbol, 6.3
-T , see --theory
- term, 6.3, 6.3, 6.3, 6.6.1
- term-case, 6.3
- term-field, 6.3
- testing WhyML code, 7.1
- then, 6.3, 6.4, 6.5.2, 6.6.2, 6.6.2
- theory, 6.5.3
- theory, 6.5.3
--theory , 5.2, 8.2.1
- tight-op, 6.1
- to, 6.6.2
- to-downto, 6.6.2
- tqualid, 6.5.3
- tr-term, 6.5.2
- trigger, 6.3, 6.5.2
- triggers, 6.3, 6.5.2
- true, 6.3, 6.4, 6.5.2
- try, 6.6.2
- type, 6.5.3, 6.5.3, 6.6.3, 6.6.3
- type, 6.2
- type-arg, 6.2
- type-case, 6.5.3
- type-decl, 6.5.3
- type-defn, 6.5.3
- type-param, 6.5.3
- uident, 6.1
- uqualid, 6.1
- use, 6.5.3
- val, 6.6.3
- variant, 6.4, 6.6.1, 6.6.2
- variant, 6.4, 6.6.1, 6.6.2
- variant-rel, 6.6.1
- wc, 5.10
- while, 6.6.2
- why3.conf, 9.3
- WhyML, 7
- with, 6.3, 6.3, 6.4, 6.4, 6.4, 6.4, 6.4, 6.5.2, 6.5.3, 6.5.3, 6.5.3, 6.5.3, 6.5.3, 6.5.3, 6.6.1, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.2, 6.6.3
- writes, 6.4, 6.4, 6.6.1, 6.6.2, 6.6.2
- writes, 6.6.1
|