REPEATC

Conv.REPEATC : conv -> conv

Repeatedly apply a conversion (zero or more times) until it fails.

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+1th 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.

Further, if c ``t`` raises the UNCHANGED exception, then REPEATC c ``t`` also raises the same exception (rather than go into an infinite loop).

Failure

Never fails, but can diverge if the supplied conversion never fails.