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
.