		Search-engine friendly clone of the ACL2 documentation.

Vl-stmt

Vl-repeatstmt

Representation of repeat statements.

This is a product type, introduced by deftagsum in support of vl-stmt.

Fields

condition — vl-expr
body — vl-stmt
atts — vl-atts: Any (* foo, bar = 1*) style attributes associated with this statement.

General Form:

repeat (<condition>)
  <body>

See Section 9.6 (page 130). The condition is presumably evaluated to a natural number, and then body is executed that many times. If the expression evaluates to X or Z, it is supposed to be treated as zero and the statement is not executed at all. (What a crock!)

Subtopics

Vl-repeatstmt->condition: Get the condition field from a vl-repeatstmt.
Make-vl-repeatstmt: Basic constructor macro for vl-repeatstmt structures.
Vl-repeatstmt->body: Get the body field from a vl-repeatstmt.
Vl-repeatstmt->atts: Get the atts field from a vl-repeatstmt.
Change-vl-repeatstmt: Modifying constructor for vl-repeatstmt structures.