		Search-engine friendly clone of the ACL2 documentation.

Proof-builder-commands

ACL2-pc::repeat

(macro) repeat the given instruction until it ``fails''

Example:
(repeat promote)

General Form:
(repeat instruction)

The given instruction is run repeatedly until it ``fails''. A call of :repeat always ``succeeds''.

Remark: There is nothing here in general to prevent the instruction from being run after all goals have been proved, though it may then fail, thus causing :repeat to return.