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
|
\DOC THENC
\TYPE {(THENC) : conv -> conv -> conv}
\SYNOPSIS
Applies two conversions in sequence.
\KEYWORDS
conversional.
\DESCRIBE
If the conversion {c1} returns {|- t = t'} when applied to a term {`t`}, and
{c2} returns {|- t' = t''} when applied to {`t'`}, then the composite
conversion {(c1 THENC c2) `t`} returns {|- t = t''}. That is, {(c1 THENC c2)
`t`} has the effect of transforming the term {`t`} first with the conversion
{c1} and then with the conversion {c2}.
\FAILURE
{(c1 THENC c2) `t`} fails if either the conversion {c1} fails when applied to
{`t`}, or if {c1 `t`} succeeds and returns {|- t = t'} but {c2} fails when
applied to {`t'`}. {(c1 THENC c2) `t`} may also fail if either of {c1} or {c2}
is not, in fact, a conversion (i.e. a function that maps a term {t} to a
theorem {|- t = t'}).
\EXAMPLE
{
# BETA_CONV `(\x. x + 1) 3`;;
val it : thm = |- (\x. x + 1) 3 = 3 + 1
# (BETA_CONV THENC NUM_ADD_CONV) `(\x. x + 1) 3`;;
val it : thm = |- (\x. x + 1) 3 = 4
}
\SEEALSO
EVERY_CONV, ORELSEC, REPEATC.
\ENDDOC
|
