Search-engine friendly clone of the
ACL2 documentation
.
Top
Lex-block-comment-loops
Lex-rest-of-block-comment
Signature
(lex-rest-of-block-comment first-pos pstate) → (mv erp last-pos new-pstate)
Arguments
first-pos
—
Guard
(
positionp
first-pos)
.
pstate
—
Guard
(
parstatep
pstate)
.
Returns
last-pos
—
Type
(
positionp
last-pos)
.
new-pstate
—
Type
(
parstatep
new-pstate)
.