EVERY_CONV : conv list -> conv
- SYNOPSIS
-
Applies in sequence all the conversions in a given list of conversions.
- DESCRIPTION
-
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 CONDITIONS
-
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
- SEE ALSO
-
THENC.