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
|
\DOC EVERY_CONV
\TYPE {EVERY_CONV : conv list -> conv}
\SYNOPSIS
Applies in sequence all the conversions in a given list of conversions.
\KEYWORDS
conversional.
\DESCRIBE
{EVERY_CONV [c1;...;cn] `t`} returns the result of applying the conversions
{c1}, ..., {cn} in sequence to the term {`t`}. The conversions are applied in
the order in which they are given in the list. In particular, if {ci `ti`}
returns {|- ti=ti+1} for {i} from {1} to {n}, then
{EVERY_CONV [c1;...;cn] `t1`} returns {|- t1=t(n+1)}. If the supplied list of
conversions is empty, then {EVERY_CONV} returns the identity conversion. That
is, {EVERY_CONV [] `t`} returns {|- t=t}.
\FAILURE
{EVERY_CONV [c1;...;cn] `t`} fails if any one of the conversions {c1}, ...,
{cn} fails when applied in sequence as specified above.
\EXAMPLE
{
# EVERY_CONV [BETA_CONV; NUM_ADD_CONV] `(\x. x + 2) 5`;;
val it : thm = |- (\x. x + 2) 5 = 7
}
\SEEALSO
THENC.
\ENDDOC
|
