		Search-engine friendly clone of the ACL2 documentation.

Vl-streamexpr

A part of the stream in a streaming operator. For instance, in {<< 16 {a, b with [0 +: size]}}, the streamexprs are a and b with [0 +: size].

This is a product type introduced by defprod.

expr — vl-expr: The expression part without the with. Example: in the expression {<< 16 {a, b with [0 +: size]}}, the exprs are a and b.
part — vl-arrayrange: The with information, if any. Example: in the expression {<< 16 {a, b with [0 +: size]}}, the part for a is the special :none arrayrange, which indicates that there is no with part. The part for b is an arrayrange that captures the [0 +: size] information.

Vl-streamexpr-equiv: Basic equivalence relation for vl-streamexpr structures.
Make-vl-streamexpr: Basic constructor macro for vl-streamexpr structures.
Vl-streamexpr->part: Get the part field from a vl-streamexpr.
Vl-streamexpr->expr: Get the expr field from a vl-streamexpr.
Change-vl-streamexpr: Modifying constructor for vl-streamexpr structures.
Vl-streamexpr-p: Recognizer for vl-streamexpr structures.
Vl-streamexprlist: A list of vl-streamexpr-p objects.
Vl-streamexpr-fix: Fixing function for vl-streamexpr structures.
Vl-streamexpr-count: Measure for recurring over vl-streamexpr structures.