Previous Up

Index

  • 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
    • of WhyML, 7.1
  • 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

Previous Up