1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
\DOC RAND_CONV
\TYPE {RAND_CONV : (conv -> conv)}
\SYNOPSIS
Applies a conversion to the operand of an application.
\KEYWORDS
conversional.
\DESCRIBE
If {c} is a conversion that maps a term {"t2"} to the theorem {|- t2 = t2'},
then the conversion {RAND_CONV c} maps applications of the form {"t1 t2"} to
theorems of the form:
{
|- (t1 t2) = (t1 t2')
}
\noindent That is, {RAND_CONV c "t1 t2"} applies {c} to the operand of the
application {"t1 t2"}.
\FAILURE
{RAND_CONV c tm} fails if {tm} is not an application or if {tm} has the form
{"t1 t2"} but the conversion {c} fails when applied to the term {t2}. The
function returned by {RAND_CONV c} may also fail if the ML function
{c:term->thm} is not, in fact, a conversion (i.e. a function that maps a term
{t} to a theorem {|- t = t'}).
\EXAMPLE
{
#RAND_CONV num_CONV "SUC 2";;
|- SUC 2 = SUC(SUC 1)
}
\SEEALSO
ABS_CONV, RATOR_CONV, SUB_CONV.
\ENDDOC
|
