		Search-engine friendly clone of the ACL2 documentation.

Seqw

An alternative implementation of the Seq language which allows for warnings to be implicitly collected and stored in a list as your program executes.

As background see seq; here we only describe the differences between Seqw and Seq.

The difference is quite straightforward:

Whereas a Seq program has the form (seq <stream> ...), a Seqw program instead has one additional argument, (seqw <stream> <warnings> ...), where <warnings> is the name of a warnings structure (see below).
Whereas every Seq action returns (mv error val stream), each Seqw action instead returns (mv error val stream warnings), where warnings is the updated warnings structure.
Similarly, every Seqw program returns (mv error val stream warnings) instead of (mv error val stream).

What is a warnings structure? When we use Seqw, we generally accumulate warnings into a list, so our actions just cons new warnings into this list when desired. But Seqw itself imposes no particular constraints on what a warnings structure is, and generally the way in which a warning is updated is determined by the actions of the program rather than by Seqw itself.

For examples of using SEQW, see the file misc/seqw-examples.lsp.