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
|
\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'}).
\SEEALSO
EVERY_CONV.
\ENDDOC
|
