In Nuprl, ` convn
` is an ML concrete type abbreviation for the type

` env -> term -> (term # reln # just)`.
` env
`, ` reln
` and ` just
` are abstract types for
* environments* , * relations
* and * justifications
*. A
conversion is a function that takes as arguments an environment
**e** and a term to be rewritten **t**, and returns a triple . The environment **e** specifies amongst other things
the types of all the variables which might be free in the term **t**.
The term is the rewritten version of the term **t**. The relation
**r** specifies the relationship between **t**
and . Writing **r** using infix notation, we can say that
is true. The relation **r** is usually some equivalence relation but it
also can be an order relation. The justification **j** is an
object that tell Nuprl
how to prove that . Conversions
fail if they are not appropriate for the term they are applied to.
More information on environments, rewrite relations, and justifications
can be found in Section
,Section
and Section

respectively.

A tactic ` Rewrite : convn -> int -> tactic` is used for applying
a conversion to some clause of a sequent. It takes care of executing
the justifications generated by conversions. Section

lists common variations on this tactic.

* Atomic* conversions are either based on direct computation rules
or can be created from lemmas and hypotheses. Conversions are
composed using higher order functions called * conversionals* in a
way similar to the way in which tactics are composed using tacticals.
One set of conversionals are for controlling the sequence in which
atomic conversions are applied to the subterms of a term.

Conversionals rely for their correct functioning on a variety of
different kinds of lemmas being proven about the relations **r** and
the terms making up any clause being rewritten; lemmas
are required that state reflexivity, transitivity and symmetry properties
of the relations **r** and congruence properties of the terms making
up the clauses. These lemmas are described in Section
.

Wed Oct 23 13:48:45 EDT 1996