# Index

Symbols | A | B | C | D | E | F | G | H | I | J | K | L | M | O | P | R | S | T | U | V | W

## Symbols

- &
- &&
- --add-provers
  - why3-session-update command line option
- --add_pp
  - why3-session-html command line option
- --apply-transform
  - why3-prove command line option
  - why3-session-create command line option
- --ce-log-verbosity
  - why3-prove command line option
- --check-ce
  - why3-prove command line option
- --color
  - why3-prove command line option
- --config
  - why3 command line option
- --context
  - why3-session-html command line option
- --coqdoc
  - why3-session-html command line option
- --debug
  - why3 command line option
- --debug-all
  - why3 command line option
- --delay
  - why3-bench command line option
- --do-not-skip-header
  - why3-wc command line option
- --driver
  - why3-extract command line option
  - why3-prove command line option
  - why3-realize command line option
- --edited-files
  - why3-session-info command line option
- --extra-config
  - why3 command line option
- --extra-expl-prefix
  - why3-prove command line option
- --factor
  - why3-wc command line option
- --filter-is-leaf
  - why3-session-update command line option
- --filter-obsolete
  - why3-session-update command line option
- --filter-proved
  - why3-session-update command line option
- --filter-prover
  - why3-session-update command line option
- --filter-status
  - why3-session-update command line option
- --flat
  - why3-extract command line option
- --force
  - why3-bench command line option
  - why3-replay command line option
- --format
  - why3-prove command line option
  - why3-realize command line option
- --goal
  - why3-prove command line option
- --graph
  - why3-session-info command line option
- --help
  - why3 command line option
- --index
  - why3-doc command line option
- --json
  - why3-prove command line option
- --library
  - why3 command line option
- --lines
  - why3-wc command line option
- --list-debug-flags
  - why3 command line option
- --longtable
  - why3-session-latex command line option
- --mark-obsolete
  - why3-session-update command line option
- --memlimit
  - why3-prove command line option
  - why3-session-create command line option
- --meta
  - why3-prove command line option
- --modular
  - why3-extract command line option
- --no-index
  - why3-doc command line option
- --no-load-default-plugins
  - why3 command line option
- --no-stdlib
  - why3 command line option
- --obsolete-only
  - why3-replay command line option
- --output
  - why3-doc command line option
  - why3-pp command line option
  - why3-realize command line option
- --output-dir
  - why3-session-create command line option
- --parse-only
  - why3-prove command line option
- --prefix
  - why3-pp command line option
- --print-datadir
  - why3 command line option
- --print-libdir
  - why3 command line option
- --print-namespace
  - why3-prove command line option
- --print-theory
  - why3-prove command line option
- --print0
  - why3-session-info command line option

- --prover
  - why3-prove command line option
  - why3-replay command line option
  - why3-session-create command line option
- --provers
  - why3-session-info command line option
- --provers-stats
  - why3-session-info command line option
- --rac
  - why3-execute command line option
- --rac-fail-cannot-check
  - why3-execute command line option
- --rac-memlimit
  - why3-execute command line option
- --rac-prover
  - why3-execute command line option
  - why3-prove command line option
- --rac-steplimit
  - why3-execute command line option
  - why3-prove command line option
- --rac-timelimit
  - why3-execute command line option
  - why3-prove command line option
- --rac-try-negate
  - why3-execute command line option
  - why3-prove command line option
- --real
  - why3-execute command line option
- --recursive
  - why3-extract command line option
- --remove-proofs
  - why3-session-update command line option
- --rename-file
  - why3-session-update command line option
- --session-stats
  - why3-session-info command line option
- --smoke-detector
  - why3-replay command line option
- --stdlib-url
  - why3-doc command line option
- --stepslimit
  - why3-prove command line option
  - why3-session-create command line option
- --style
  - why3-session-html command line option
  - why3-session-latex command line option
- --sub-goal
  - why3-prove command line option
- --theory
  - why3-prove command line option
  - why3-realize command line option
- --timelimit
  - why3-prove command line option
  - why3-session-create command line option
- --title
  - why3-doc command line option
- --tokens
  - why3-wc command line option
- --type-only
  - why3-prove command line option
- --use
  - why3-execute command line option
- -a
  - why3-prove command line option
  - why3-session-create command line option
  - why3-wc command line option
- -C
  - why3 command line option
- -D
  - why3-extract command line option
  - why3-prove command line option
  - why3-realize command line option
- -d
  - why3-bench command line option
- -e
  - why3-session-latex command line option
- -F
  - why3-prove command line option
  - why3-realize command line option
- -f
  - why3-bench command line option
  - why3-wc command line option
- -G
  - why3-prove command line option
- -g
  - why3-prove command line option
- -L
  - why3 command line option
- -l
  - why3-wc command line option
- -m
  - why3-session-create command line option
- -o
  - why3-doc command line option
  - why3-extract command line option
  - why3-realize command line option
  - why3-session-create command line option
  - why3-session-html command line option
  - why3-session-latex command line option
- -P
  - why3-prove command line option
  - why3-session-create command line option
- -q
  - why3-replay command line option
- -s
  - why3-replay command line option
  - why3-session-create command line option
- -T
  - why3-prove command line option
  - why3-realize command line option
- -t
  - why3-session-create command line option
  - why3-wc command line option
- ||

## A

- abstract
  - keyword
- abstract type
- algebraic data type
- any
  - keyword
- apply
  - transformation
- apply with
  - transformation
- assert
  - transformation
- assert as
  - transformation
- assignment expressions
- at
  - keyword
- attribute
  - case_split
  - cfg:stackify
  - cfg:subregion_analysis
  - extraction:inline
  - extraction:likely
  - extraction:preserve_single_field
  - extraction:unlikely
  - induction
  - infer
  - inline:trivial
  - java:class_kind:
  - java:constructor
  - java:exception:
  - java:implements:
  - java:package:
  - java:visibility:package
  - java:visibility:private
  - java:visibility:public
  - model_trace
  - rewrite
  - stop_split
  - vc:annotation
  - vc:divergent
  - vc:keep_precondition
  - vc:sp
  - vc:white_box
  - vc:wp

- auto-dereference, [1], [2]

## B

- bench
  - command
- bracket

- break
  - keyword
- by
  - keyword

## C

- case
  - transformation
- case as
  - transformation
- case_split
  - attribute
- CFG
- cfg:stackify
  - attribute
- cfg:subregion_analysis
  - attribute
- clear_but
  - transformation
- clone
  - keyword
- collections, [1]
- Coma
- command
  - bench
  - config
  - config add-prover
  - config detect
  - config list-provers
  - config list-supported-provers
  - config show
  - doc
  - execute
  - extract
  - ide
  - pp
  - prove
  - realize
  - replay
  - session
  - session create
  - session html
  - session info
  - session latex
  - session update
  - show
  - show attributes
  - show formats
  - show metas
  - show printers
  - show transformations
  - wc

- compute_hyp
  - transformation
- compute_hyp_specified
  - transformation
- compute_in_goal
  - transformation
- compute_max_steps
  - meta
- compute_specified
  - transformation
- conditional
- config
  - command
- config add-prover
  - command
- config detect
  - command
- config list-provers
  - command
- config list-supported-provers
  - command
- config show
  - command
- configuration file, [1]
- continue
  - keyword
- Coq proof assistant
- cut
  - transformation

## D

- debug flag
  - infer:loop
  - infer:print_ai_result
  - infer:print_cfg
  - print:domains_loop
  - print:inferred_invs
  - stack_trace
- destruct
  - transformation
- destruct_rec
  - transformation

- destruct_term
  - transformation
- destruct_term using
  - transformation
- destruct_term_subst
  - transformation
- detached
- doc
  - command
- downto
  - keyword
- driver file

## E

- Einstein’s problem
- eliminate_algebraic
  - transformation
- eliminate_builtin
  - transformation
- eliminate_definition
  - transformation
- eliminate_definition_func
  - transformation
- eliminate_definition_pred
  - transformation
- eliminate_if
  - transformation
- eliminate_if_fmla
  - transformation
- eliminate_if_term
  - transformation
- eliminate_inductive
  - transformation
- eliminate_let
  - transformation
- eliminate_let_fmla
  - transformation
- eliminate_let_term
  - transformation
- eliminate_literal
  - transformation
- eliminate_mutual_recursion
  - transformation

- eliminate_recursion
  - transformation
- else
  - keyword
- encoding_smt
  - transformation
- encoding_tptp
  - transformation
- environment variable
  - PATH, [1]
  - WHY3CONFIG, [1]
  - WHY3DATA
  - WHY3LIB
- evaluation order
- execute
  - command
- exists
  - transformation
- extract
  - command
- extraction:inline
  - attribute
- extraction:likely
  - attribute
- extraction:preserve_single_field
  - attribute
- extraction:unlikely
  - attribute

## F

- float
  - keyword
- for
  - keyword, [1]

- for each loop
- function
  - keyword
- function literals, [1]

## G

- ghost
  - keyword, [1]

## H

- hide
  - transformation

- hide_and_clear
  - transformation

## I

- ide
  - command
- if
  - keyword
- induction
  - attribute
  - transformation
- induction from
  - transformation
- induction_arg_pr
  - transformation
- induction_arg_ty_lex
  - transformation
- induction_pr
  - transformation
- induction_ty_lex
  - transformation
- infer
  - attribute
- infer:loop
  - debug flag
- infer:print_ai_result
  - debug flag
- infer:print_cfg
  - debug flag
- inline:trivial
  - attribute

- inline_all
  - transformation
- inline_goal
  - transformation
- inline_trivial
  - transformation
- inst_rem
  - transformation
- instantiate
  - transformation
- introduce_premises
  - transformation
- intros
  - transformation
- intros_n
  - transformation
- invariant
  - for each loop
  - for loop
  - keyword, [1], [2]
  - type
- inversion_arg_pr
  - transformation
- inversion_pr
  - transformation
- Isabelle proof assistant

## J

- java:class_kind:
  - attribute
- java:constructor
  - attribute
- java:exception:
  - attribute
- java:implements:
  - attribute

- java:package:
  - attribute
- java:visibility:package
  - attribute
- java:visibility:private
  - attribute
- java:visibility:public
  - attribute

## K

- keep:literal
  - meta
- keyword
  - abstract
  - any
  - at
  - break
  - by
  - clone
  - continue
  - downto
  - else
  - float
  - for, [1]
  - function
  - ghost, [1]
  - if
  - invariant, [1], [2]
  - label
  - let, [1]
  - old
  - partial
  - predicate
  - private
  - range
  - rec
  - ref
  - so
  - then
  - val
  - variant
  - while

## L

- label
  - keyword
- left
  - transformation

- let
  - keyword, [1]

## M

- mapping type
- meta
  - compute_max_steps
  - keep:literal
  - realized_theory
  - rewrite
  - rewrite_def
  - vc:proved_wf

- micro-C
- model_trace
  - attribute
- module cloning

## O

- obsolete, [1], [2]

- old
  - keyword

## P

- partial
  - keyword
- PATH, [1]
- pattern-matching
- pose
  - transformation
- pp
  - command
- predicate
  - keyword
- print:domains_loop
  - debug flag

- print:inferred_invs
  - debug flag
- private
  - keyword
- private type
- proof assistant
  - Coq
  - Isabelle
  - PVS
- prove
  - command
- PVS proof assistant
- Python

## R

- range
  - keyword
- range type
- realize
  - command
- realized_theory
  - meta
- rec
  - keyword
- record type
- ref
  - keyword
- reference
- remove
  - transformation
- remove_unused
  - transformation
- remove_unused_keep_constant
  - transformation

- replace
  - transformation
- replay
  - command
- revert
  - transformation
- rewrite
  - attribute
  - meta
  - transformation
- rewrite with
  - transformation
- rewrite_def
  - meta
- rewrite_list
  - transformation
- right
  - transformation

## S

- S-expressions
- session
  - command
- session create
  - command
- session html
  - command
- session info
  - command
- session latex
  - command
- session update
  - command
- show
  - command
- show attributes
  - command
- show formats
  - command
- show metas
  - command
- show printers
  - command
- show transformations
  - command
- simplify_array
  - transformation
- simplify_formula
  - transformation
- simplify_formula_and_task
  - transformation

- simplify_recursive_definition
  - transformation
- simplify_trivial_quantification
  - transformation
- simplify_trivial_quantification_in_goal
  - transformation
- snapshot type
- so
  - keyword
- split_all
  - transformation
- split_all_full
  - transformation
- split_goal
  - transformation
- split_goal_full
  - transformation
- split_intro
  - transformation
- split_premise
  - transformation
- split_premise_full
  - transformation
- stack_trace
  - debug flag
- standard library
- stop_split
  - attribute
- subst
  - transformation
- subst_all
  - transformation

## T

- then
  - keyword
- transformation
  - apply
  - apply with
  - assert
  - assert as
  - case
  - case as
  - clear_but
  - compute_hyp
  - compute_hyp_specified
  - compute_in_goal
  - compute_specified
  - cut
  - destruct
  - destruct_rec
  - destruct_term
  - destruct_term using
  - destruct_term_subst
  - eliminate_algebraic
  - eliminate_builtin
  - eliminate_definition
  - eliminate_definition_func
  - eliminate_definition_pred
  - eliminate_if
  - eliminate_if_fmla
  - eliminate_if_term
  - eliminate_inductive
  - eliminate_let
  - eliminate_let_fmla
  - eliminate_let_term
  - eliminate_literal
  - eliminate_mutual_recursion
  - eliminate_recursion
  - encoding_smt
  - encoding_tptp
  - exists
  - hide
  - hide_and_clear
  - induction
  - induction from
  - induction_arg_pr
  - induction_arg_ty_lex
  - induction_pr
  - induction_ty_lex
  - inline_all
  - inline_goal
  - inline_trivial
  - inst_rem
  - instantiate
  - introduce_premises
  - intros
  - intros_n
  - inversion_arg_pr
  - inversion_pr
  - left
  - pose
  - remove
  - remove_unused
  - remove_unused_keep_constant
  - replace
  - revert
  - rewrite
  - rewrite with
  - rewrite_list
  - right
  - simplify_array
  - simplify_formula
  - simplify_formula_and_task
  - simplify_recursive_definition
  - simplify_trivial_quantification
  - simplify_trivial_quantification_in_goal
  - split_all
  - split_all_full
  - split_goal
  - split_goal_full
  - split_intro
  - split_premise
  - split_premise_full
  - subst
  - subst_all
  - unfold
  - use_th

- tuples
- type invariant

## U

- unfold
  - transformation

- use_th
  - transformation

## V

- val
  - keyword
- variant
  - keyword
- vc:annotation
  - attribute
- vc:divergent
  - attribute
- vc:keep_precondition
  - attribute

- vc:proved_wf
  - meta
- vc:sp
  - attribute
- vc:white_box
  - attribute
- vc:wp
  - attribute

## W

- wc
  - command
- while
  - keyword
- why3 command line option
  - --config
  - --debug
  - --debug-all
  - --extra-config
  - --help
  - --library
  - --list-debug-flags
  - --no-load-default-plugins
  - --no-stdlib
  - --print-datadir
  - --print-libdir
  - -C
  - -L
- why3-bench command line option
  - --delay
  - --force
  - -d
  - -f
- why3-doc command line option
  - --index
  - --no-index
  - --output
  - --stdlib-url
  - --title
  - -o
- why3-execute command line option
  - --rac
  - --rac-fail-cannot-check
  - --rac-memlimit
  - --rac-prover
  - --rac-steplimit
  - --rac-timelimit
  - --rac-try-negate
  - --real
  - --use
- why3-extract command line option
  - --driver
  - --flat
  - --modular
  - --recursive
  - -D
  - -o
- why3-pp command line option
  - --output
  - --prefix
- why3-prove command line option
  - --apply-transform
  - --ce-log-verbosity
  - --check-ce
  - --color
  - --driver
  - --extra-expl-prefix
  - --format
  - --goal
  - --json
  - --memlimit
  - --meta
  - --parse-only
  - --print-namespace
  - --print-theory
  - --prover
  - --rac-prover
  - --rac-steplimit
  - --rac-timelimit
  - --rac-try-negate
  - --stepslimit
  - --sub-goal
  - --theory
  - --timelimit
  - --type-only
  - -a
  - -D
  - -F
  - -G
  - -g
  - -P
  - -T

- why3-realize command line option
  - --driver
  - --format
  - --output
  - --theory
  - -D
  - -F
  - -o
  - -T
- why3-replay command line option
  - --force
  - --obsolete-only
  - --prover
  - --smoke-detector
  - -q
  - -s
- why3-session-create command line option
  - --apply-transform
  - --memlimit
  - --output-dir
  - --prover
  - --stepslimit
  - --timelimit
  - -a
  - -m
  - -o
  - -P
  - -s
  - -t
- why3-session-html command line option
  - --add_pp
  - --context
  - --coqdoc
  - --style
  - -o
- why3-session-info command line option
  - --edited-files
  - --graph
  - --print0
  - --provers
  - --provers-stats
  - --session-stats
- why3-session-latex command line option
  - --longtable
  - --style
  - -e
  - -o
- why3-session-update command line option
  - --add-provers
  - --filter-is-leaf
  - --filter-obsolete
  - --filter-proved
  - --filter-prover
  - --filter-status
  - --mark-obsolete
  - --remove-proofs
  - --rename-file
- why3-wc command line option
  - --do-not-skip-header
  - --factor
  - --lines
  - --tokens
  - -a
  - -f
  - -l
  - -t
- WHY3CONFIG