Index

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
- proof attempt, 5.3.1
--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
- of WhyML, 7.1
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
- proof attempt, 1.2.3, 5.3.1, 5.4
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