Also see the ML Manual for Nuprl4.

Writing complicated tactics requires a thorough knowledge of the ML programming language [Gordon, Milner, & Wadsworth 79] and the information contained in chapter 9. It is an easy matter, however, to write simple tactics and to combine existing tactics with a minimal subset of ML. ML is a functional programming language with three important characteristics which make it a good language for expressing tactics:

- ML has an extensible, polymorphic
type discipline with secure types. This allows type constraints on the arguments and results of functions to be expressed and enforced. For example, the result of a function may be constrained to be of type

`proof`. - ML has a mechanism for raising and handling
exceptions (or, in the
terminology of ML, throwing and catching failures). This is a convenient
way to incorporate backtracking into tactics.
- ML is fully higher--order; functions are objects in the language. This allows tactics (which are functions) to be combined using combining forms called tacticals, all of which are written in ML.

In order to understand the example tactics presented below it is not necessary to know many of the details of ML. The following summarizes some of the more important and less obvious language constructs. Functions in ML are defined as in

let divides x y = ((x/y)*y = x);;

` intintbool`; that is,
it maps integers to functions from integers to boolean values. There is
also an explicit abstraction operator,
, which stands for the more
conventional . The previous function
could have been defined as

let divides = \ x . \ y . ((x/y)*y = x);;

Exceptions
are raised using the expression
``` fail`'' and handled (*
caught*) using ``?''. The result of evaluating * exp1?exp2* is the
result of evaluating * exp1* unless a failure is encountered, in
which case it is the result of evaluating * exp2*.
For example, the following function returns * false* if **y = 0**.

let divides x y = (if y = 0 then fail else (y*(x/y)=x) ) ? false;;

In fact, because dividing by **0** causes a failure, we could define the same
function with

let divides x y = (y*(x/y)=x)?false;;

Thu Sep 14 08:45:18 EDT 1995