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
|
\DOC FIRST_CONV
\TYPE {FIRST_CONV : conv list -> conv}
\SYNOPSIS
Apply the first of the conversions in a given list that succeeds.
\KEYWORDS
conversional.
\DESCRIBE
{FIRST_CONV [c1;...;cn] `t`} returns the result of applying to the term {`t`}
the first conversion {ci} that succeeds when applied to {`t`}. The conversions
are tried in the order in which they are given in the list.
\FAILURE
{FIRST_CONV [c1;...;cn] `t`} fails if all the conversions {c1}, ..., {cn} fail
when applied to the term {`t`}. {FIRST_CONV cs `t`} also fails if {cs} is the
empty list.
\EXAMPLE
{
# FIRST_CONV [NUM_ADD_CONV; NUM_MULT_CONV; NUM_EXP_CONV] `12 * 12`;;
val it : thm = |- 12 * 12 = 144
}
\SEEALSO
ORELSEC.
\ENDDOC
|
