Producing formulas

To output a formula (which fits on one line), you use \[ ... \] or \{ ... \}. The first form will print the formula in a mathematical version (like ). The second will produce a verbatim version, using the syntax (like /\X (X -> X)). The second form is useful when producing a documentation for a library, when you have to teach your reader the syntax you use.

Formulas produced by \[ ... \] may be broken by TeX using its usual breaking scheme. Formula produced by \{ ... \} will never be broken (because LaTeX do not insert break inside a box produced by \verb). We will see later how to produce larger formulas.

LaTeX formulas can use extra goodies:

• They can contain free variables.

• If A is a defined symbol in , $$A will refer to the definition of A (If this definition is applied to arguments, the result will be normalised before printing). Remember that a single dollar must be used when as a special syntax and you want just to refer to (For instance you use $+ to refer to the addition symbol when it is not applied to two arguments).

• All the hypothesis of the current goal are treated like any defined symbol.

• $0 refers to the conclusion of the current goal.

• You can use the form \[n or \{n where n is an integer to access the conclusion and the hypothesis of the nth goal to prove (instead of the current goal).

• You can use the following flags (see the index B for a more detailed description) to control how formulas will look like: binder_tex_space, comma_tex_space, min_tex_space, max_tex_space, tex_indent,
tex_lisp_app, tex_type_sugar, tex_margin, tex_max_indent

A \[ ... \] or \{ ... \} can be used both in text mode and in math mode. If you are in text mode, \[ ... \] is equivalent to $\[ ... \]$ (idem with curly braces).

WARNING: the closing of a formula: \], \} should not be immediately followed by a character such that this closing plus this character is a valid identifier for . Good practice is always to follow it by a white space. This is a very common error!