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 RATOR_CONV
\TYPE {RATOR_CONV : conv -> conv}
\SYNOPSIS
Applies a conversion to the operator of an application.
\KEYWORDS
conversional.
\DESCRIBE
If {c} is a conversion that maps a term {`t1`} to the theorem {|- t1 = t1'},
then the conversion {RATOR_CONV c} maps applications of the form {`t1 t2`} to
theorems of the form:
{
|- (t1 t2) = (t1' t2)
}
\noindent That is, {RATOR_CONV c `t1 t2`} applies {c} to the operator of the
application {`t1 t2`}.
\FAILURE
{RATOR_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 {t1}. The
function returned by {RATOR_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
{
# RATOR_CONV BETA_CONV `(\x y. x + y) 1 2`;;
val it : thm = |- (\x y. x + y) 1 2 = (\y. 1 + y) 2
}
\SEEALSO
ABS_CONV, COMB_CONV, COMB2_CONV, RAND_CONV, SUB_CONV.
\ENDDOC
|
