-
API, 3, 4.1.2
-a, see --apply-transform
--add-prover, 4.2.1, 5.1
--apply-transform, 5.2
-C, see --config
- Coq proof assistant, 8.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
-D, see --driver
--debug, 5
--debug-all, 5
- detached
--detect-plugins, 5.1
--detect-provers, 5.1
--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
encoding_smt, 9.5.4
encoding_tptp, 9.5.4
- execute, 5.7, 7.1
--extra-config, 5, 8.2.3
- extract, 5.8, 7.2
- extraction, 7.2
-G, see --goal
--goal, 5.2
--help, 5
- Isabelle proof assistant, 8.4
- ide, 5.3
induction_ty_lex, 9.5.2
| inline_all, 9.5.1
inline_goal, 9.5.1
inline_trivial, 9.5.1
- interpretation
introduce_premises, 9.5.4
-L, see --library
--library, 5
--list-debug-flags, 5
--list-formats, 5, 5.2
--list-metas, 5
--list-printers, 5
--list-prover-ids, 5.1
--list-provers, 1.3, 5, 5.2
--list-transforms, 5, 5.2, 9.5
- OCaml, 7.2
- obsolete
option, 8.2.3
-P, see --prover
- PVS proof assistant, 8.5
- plugin, 5.1
- prove, 5.2
--prover, 5.2
prover_modifiers, 8.2.3
- realize, 5.9, 8.2.1
realized_theory, 8.2.2
- replay, 5.4
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
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
-T, see --theory
- testing WhyML code, 7.1
--theory, 5.2, 8.2.1
- wc, 5.10
- why3.conf, 9.3
- WhyML, 7
|
