Index

0B, 7.1.4
0b, 7.1.4
0O, 7.1.4
0o, 7.1.4
0X, 7.1.4, 7.1.4
0x, 7.1.4, 7.1.4
_, 7.1.3, 7.1.3, 7.1.4, 7.1.4, 7.1.4, 7.1.4, 7.2.1
API, 4, 5.3
-a, see --apply-transform
abstract, 7.3.2
absurd, 7.3.1
--add-prover, 5.5, 6.1
alpha, 7.1.3
alpha-no-us, 7.1.3
any, 7.3.2
--apply-transform, 6.2
archived, 5.6
- proof attempt, 6.3.1, 6.6
as, 7.2.1, 7.2.4, 7.2.4
assert, 7.3.1
assertion, 7.3.1
assume, 7.3.1
at, 7.3.1
axiom, 7.2.4
bang-op, 7.1.5
bin-digit, 7.1.4
binder, 7.3.2
binders, 7.2.3
by, 7.2.3
-C, see --config
Coq proof assistant, 9.3
check, 7.3.1
clone, 7.2.4
coinductive, 7.2.4
compute_in_goal, 10.5.3
compute_specified, 10.5.3
config, 6.1
--config, 6
configuration file, 6.1, 9.2.3, 10.3
constant, 7.2.4
constant-decl, 7.2.4
-D, see --driver
--debug, 6
--debug-all, 6
decl, 7.2.4
--detect-plugins, 6.1
--detect-provers, 6.1
digit, 7.1.4
digit-or-us, 7.1.3
do, 7.3.2, 7.3.2
done, 7.3.2, 7.3.2
downto, 7.3.2
--driver, 6.2, 9.2.1
driver, 9.2.3
driver file, 9.2.2
Einstein’s logic problem, 2.3
editor_modifiers, 9.2.3
eliminate_algebraic, 10.5.4
eliminate_builtin, 10.5.4
eliminate_definition, 10.5.4
eliminate_definition_func, 10.5.4
eliminate_definition_pred, 10.5.4
eliminate_if, 10.5.4
eliminate_if_fmla, 10.5.4
eliminate_if_term, 10.5.4
eliminate_inductive, 10.5.4
eliminate_let, 10.5.4
eliminate_let_fmla, 10.5.4
eliminate_let_term, 10.5.4
eliminate_mutual_recursion, 10.5.4
eliminate_recursion, 10.5.4
else, 7.2.1, 7.2.3, 7.3.2
encoding_smt, 10.5.4
encoding_tptp, 10.5.4
end, 7.2.1, 7.2.3, 7.2.4, 7.2.4, 7.3.2, 7.3.2, 7.3.2, 7.3.3, 7.3.3
ensures, 7.3.1
ensures, 7.3.1
exception, 7.3.3
execute, 6.8, 8.1
exists, 7.2.3
exponent, 7.1.4
export, 7.2.4
expr, 7.3.2
expr-case, 7.3.2
expr-field, 7.3.2
--extra-config, 6, 9.2.3
extract, 6.9, 8.2
extraction, 8.2
false, 7.2.3
file, 7.2.5, 7.3.4
filename, 7.1.6
float, 7.2.4
for, 7.3.2
forall, 7.2.3
formula, 7.2.3
formula-case, 7.2.3
fun, 7.3.2, 7.3.3
fun-body, 7.3.2
fun-defn, 7.3.2
function, 7.2.4, 7.2.4
function-decl, 7.2.4
-G, see --goal
ghost, 7.3.2, 7.3.2, 7.3.2, 7.3.2, 7.3.3, 7.3.3, 7.3.3
goal, 7.2.4, 7.2.4
--goal, 6.2
h-exponent, 7.1.4
handler, 7.3.2
--help, 6
hex-digit, 7.1.4
hex-real, 7.1.4
Isabelle proof assistant, 9.4
ide, 6.3
ident, 7.1.3
ident-nq, 7.1.3
if, 7.2.1, 7.2.3, 7.3.2
imp-exp, 7.2.4
import, 7.2.4, 7.2.4, 7.3.3
in, 7.2.1, 7.2.3, 7.3.2, 7.3.2, 7.3.2
ind-case, 7.2.4
induction_ty_lex, 10.5.2
inductive, 7.2.4
inductive-decl, 7.2.4
infix-op, 7.1.5
infix-op-, 7.1.5
inline_all, 10.5.1
inline_goal, 10.5.1
inline_trivial, 10.5.1
integer, 7.1.4
interpretation
- of WhyML, 8.1
introduce_premises, 10.5.4
invariant, 7.3.1

invariant, 7.3.1
-L, see --library
label, 7.1.6
lalpha, 7.1.3
lemma, 7.2.4, 7.2.4
let, 7.2.1, 7.2.3, 7.3.2, 7.3.2, 7.3.2, 7.3.3, 7.3.3
library, 7.4
--library, 6
lident, 7.1.3
lident-nq, 7.1.3
--list-debug-flags, 6
--list-formats, 6.2
--list-prover-ids, 6.1
--list-provers, 1.3, 6.2, 9.3.1
--list-transforms, 6.2, 10.5
logic-decl, 7.2.4
loop, 7.3.2
lqualid, 7.1.3
match, 7.2.1, 7.2.3, 7.3.2
mdecl, 7.3.3
module, 7.3.3
module, 7.3.3
mrecord-field, 7.3.3
mtype-decl, 7.3.3
mtype-defn, 7.3.3
mutable, 7.3.3
namespace, 7.2.4, 7.2.4, 7.3.3
not, 7.2.3
OCaml, 8.2
obsolete
- proof attempt, 1.2.3, 6.3.1, 6.5
oct-digit, 7.1.4
old, 7.3.1
one-variant, 7.3.1
op-char, 7.1.5
op-char-, 7.1.5, 7.1.5, 7.1.5, 7.1.5
option, 9.2.3
-P, see --prover
PVS proof assistant, 9.5
param, 7.3.2
pattern, 7.2.1
pgm-decl, 7.3.3
pgm-defn, 7.3.3
plugin, 6.1
predicate, 7.2.4, 7.2.4
predicate-decl, 7.2.4
prefix-op, 7.1.5
prove, 6.2
--prover, 6.2
prover_modifiers, 9.2.3
qualid, 7.1.3
quantifier, 7.2.3
raise, 7.3.2, 7.3.2
raises, 7.3.1, 7.3.1
raises, 7.3.1
raises-case, 7.3.1
range, 7.2.4
reads, 7.3.1
reads, 7.3.1
real, 7.1.4
realize, 6.10, 9.2.1
realized_theory, 9.2.2
rec, 7.3.2, 7.3.3
rec-defn, 7.3.2
record-field, 7.2.4
replay, 6.5
requires, 7.3.1
requires, 7.3.1
returns, 7.3.1
returns, 7.3.1
simplify_array, 10.5.4
simplify_formula, 10.5.4
simplify_formula_and_task, 10.5.5
simplify_recursive_definition, 10.5.4
simplify_trivial_quantification, 10.5.4
simplify_trivial_quantification_in_goal, 10.5.4
so, 7.2.3
spec, 7.3.1
split_all, 10.5.5
split_all_full, 10.5.5
split_goal, 10.5.5
split_goal_full, 10.5.5
split_intro, 10.5.5
split_premise, 10.5.4
split_premise_full, 10.5.4
standard library, 7.4
subst, 7.2.4
subst-elt, 7.2.4
suffix, 7.1.3
suffix-nq, 7.1.3
-T, see --theory
term, 7.2.1, 7.3.1
term-case, 7.2.1
term-field, 7.2.1
testing WhyML code, 8.1
then, 7.2.1, 7.2.3, 7.3.2
theory, 7.2.4
theory, 7.2.4
--theory, 6.2, 9.2.1
to, 7.3.2
to-downto, 7.3.2
tqualid, 7.2.4
tr-term, 7.2.3
trigger, 7.2.3
triggers, 7.2.3
true, 7.2.3
try, 7.3.2
type, 7.2.4, 7.2.4, 7.3.3, 7.3.3
type, 7.2.2
type-case, 7.2.4
type-decl, 7.2.4
type-defn, 7.2.4
type-param, 7.2.4
ualpha, 7.1.3
uident, 7.1.3
uident-nq, 7.1.3
uqualid, 7.1.3
use, 7.2.4
val, 7.3.3
variant, 7.3.1
variant, 7.3.1
variant-rel, 7.3.1
wc, 6.11
while, 7.3.2
why3.conf, 10.3
WhyML, 8
with, 7.2.1, 7.2.1, 7.2.3, 7.2.4, 7.2.4, 7.2.4, 7.2.4, 7.2.4, 7.2.4, 7.3.1, 7.3.2, 7.3.2, 7.3.2, 7.3.2, 7.3.3
writes, 7.3.1
writes, 7.3.1