		Search-engine friendly clone of the ACL2 documentation.

Vl-binddelta

Vl-bindintent

An intent to bind additional submodules, and where it comes from.

This is a product type introduced by defprod.

Fields

source — vl-bind: Original bind that led to this.
ctx — vl-bindcontext: Where that bind came from.

The module we're intending to add these to is not included because that will be put in the vl-binddelta. The module instances we're adding are found inside the source, of course.

Subtopics

Vl-bindintent-fix: Fixing function for vl-bindintent structures.
Vl-bindintent-equiv: Basic equivalence relation for vl-bindintent structures.
Make-vl-bindintent: Basic constructor macro for vl-bindintent structures.
Vl-bindintent->source: Get the source field from a vl-bindintent.
Vl-bindintent->ctx: Get the ctx field from a vl-bindintent.
Change-vl-bindintent: Modifying constructor for vl-bindintent structures.
Vl-bindintent-p: Recognizer for vl-bindintent structures.