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
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 .