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
|
\DOC REPEATC
\TYPE {REPEATC : conv -> conv}
\SYNOPSIS
Repeatedly apply a conversion (zero or more times) until it fails.
\KEYWORDS
conversional.
\DESCRIBE
If {c} is a conversion effects a transformation of a term {t} to a term {t'},
that is if {c} maps {t} to the theorem {|- t = t`}, then {REPEATC c} is the
conversion that repeats this transformation as often as possible. More
exactly, if {c} maps the term {`ti`} to {|- ti=t(i+1)} for {i} from {1} to {n},
but fails when applied to the {n+1}th term {`t(n+1)`}, then {REPEATC c `t1`}
returns {|- t1 = t(n+1)}. And if {c `t`} fails, them {REPEATC c `t`} returns
{|- t = t}.
\FAILURE
Never fails, but can diverge if the supplied conversion never fails.
\EXAMPLE
{
# BETA_CONV `(\x. (\y. x + y) (x + 1)) 1`;;
val it : thm = |- (\x. (\y. x + y) (x + 1)) 1 = (\y. 1 + y) (1 + 1)
# REPEATC BETA_CONV `(\x. (\y. x + y) (x + 1)) 1`;;
val it : thm = |- (\x. (\y. x + y) (x + 1)) 1 = 1 + 1 + 1
}
\ENDDOC
|
