		Search-engine friendly clone of the ACL2 documentation.

Vl-lucidocc

Vl-lucidocc-slice

An indexed occurrence of an identifier.

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

Fields

left — vl-expr
right — vl-expr
ctx — vl-lucidctx: The general context where the usage occurred. Knowing where the occurrence came from is useful when we need to report about multiply driven signals.

We use this to record occurrences of an identifier with a bit- or part-select. For individual selects like foo[3], both left and right will be the same.

Subtopics

Make-vl-lucidocc-slice: Basic constructor macro for vl-lucidocc-slice structures.
Vl-lucidocc-slice->right: Get the right field from a vl-lucidocc-slice.
Vl-lucidocc-slice->left: Get the left field from a vl-lucidocc-slice.
Vl-lucidocc-slice->ctx: Get the ctx field from a vl-lucidocc-slice.
Change-vl-lucidocc-slice: Modifying constructor for vl-lucidocc-slice structures.