Flags index.

In this index we list all the flags (see the description of the command flag in the index A to learn how to print and modify the value of these flags).

auto_lvl

(integer, default is 0) : Control the automatic detection of axioms: If it is set to 0 no detection is performed. If it is set to 1, axioms are detected when the goal is structurally equal to an hypothesis. If it is set to 2, axioms are detected when the goal unifies is equal to an hypothesis up to the expansion of some definitions. If it is set to 3, axioms are detected if the goal unifies with an hypothesis (using no equations). We recommend avoiding 3 as it may instantiate variables with the wrong value.

auto_type

(bool, default is false) : automatically apply all the introduction rule which were introduced with the flags -i and -c or -t. We recommend setting this flag to true and using auto_lvl set to 2 to solve automatically all the ``typing'' goals (like proving that something is an integer).

binder_tex_space

(integer, default is 3) : set the space after a binder when is printing TeX formulas.

comma_tex_space

(integer, default is 5) : set the space after punctuation when is printing TeX formulas.

ellipsis_text

(string, default is ``...'') : the text to be printed when an expression is too deep (used by the pretty printer only).

eq_breadth

(integer, default is 4) : maximum number of equations used at each step of rewriting.

eq_flvl

(integer, default is 3) : maximum number of interleaved equations tried without decreasing the distance (the rewriting algorithm uses a distance between first order terms).

eq_depth

(integer, default is 100) : maximum number of interleaved equations applied by the rewriting algorithm.

margin

(integer, default is 80) : size of the page (used by the pretty printer only).

max_indent

(integer, default is 50) : maximum number of indentation (used by the pretty printer only).

max_boxes

(integer, default is 100) : control the maximum printing ``depth''. If the expression is too deep, an ellipsis is printed (used by the pretty printer only).

min_tex_space

(integer, default is 20) : set the minimum space (in 100th of em) between to tokens when is printing TeX formulas.

max_tex_space

(integer, default is 40) : set the minimum space (in 100th of em) between to tokens when is printing TeX formulas.

tex_indent

(integer, default is 200) : set the indentation space (in 100th of em) used by when printing multi-lines TeX formulas.

tex_lisp_app

(boolean, default is true) : If true the syntax is used for application when producing LaTeX formulas. If false, the syntax is used.

tex_type_sugar

(boolean, default is true) : If true the syntactic sugar for is used when producing LaTeX formulas.

tex_margin

(integer, default is 80) : size of the page used when printing verbatim formulas in TeX.

tex_max_indent

(integer, default is 50) : maximum number of indentation used when printing verbatim formulas in TeX.

trivial_depth

(integer, default is 4) : default value for the trivial command.