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
37
|
\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} 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`;;
val it : thm = |- SUC 2 = SUC (SUC 1)
}
\SEEALSO
ABS_CONV, COMB_CONV, COMB_CONV2, LAND_CONV, RATOR_CONV, SUB_CONV.
\ENDDOC
|
