Tactic Arguments

Unlike Lisp functions, ML functions cannot take optional arguments  , although it is natural to want to write tactics which do take optional arguments. One approach is to provide a set of variants of each tactic for the most common combinations of arguments. This can be confusing, and places an extra burden on the user who has to keep track of these variants. Nuprl V4 allows optional arguments to be passed to tactics by attaching these arguments to the proof argument which all tactics operate on. Currently argument types of int, tactic, term, tok, var and (var # term) list are supported. Each argument is given a token label, and arguments are looked up by these labels. Sets of arguments are maintained on a stack, so nesting of tactics which use optional arguments is possible.

Note that some tactics do useful preprocessing on some of their arguments, and in these cases there would be a performance penalty if such arguments were supplied, annotated to the proof.

Tactic arguments  are also used for the analogy tactics . See the relevant section below.

Tacticals for manipulating these arguments are:

With (t:term) T

Runs T with t as a `t1` argument.

Runs T with v1 to vn as arguments `v1` to `vn`.

Runs T with U as a `universe` argument. Term U should either be either a type universe or a propositional universe term.

Runs T with the substitution sub as a sub argument.

Runs T with the integer n as an n argument. Used for selecting a simple component of a universal formula or a subterm of a term.

These tactics are all special cases of:

WithArgs (args: (tok # arg) list) T

Run T with the arguments in args on the top of the stack. arg is an ML abstract data type, defined as the disjoint union of the types listed above. There exist injection and projection functions for each of the types listed above.

Each tactic description includes information on the optional arguments (if any) that it takes.