		Search-engine friendly clone of the ACL2 documentation.

Address

This is a product type, introduced by defflexsum in support of address.

Svarlist-add-delay: (svarlist-add-delay x delay) maps svar-add-delay across a list.
Svarlist-addr-p: (svarlist-addr-p x) recognizes lists where every element satisfies svar-addr-p.
Address-fix: Fixing function for address structures.
Svex-alist-add-delay
Svarlist-addr-p-badguy
Svar-add-delay
Make-scoped-svar: Make an svar for a name under a single scope level, e.g. foo.bar
Address-p: Recognizer for address structures.
Address-equiv: Basic equivalence relation for address structures.
Make-address: Basic constructor macro for address structures.
Svar-addr-p: An svar containing an address.
Svar-addr-fix
Change-address: Modifying constructor for address structures.
Address->scope: Get the scope field from a address.
Address->path: Get the path field from a address.
Address->index: Get the index field from a address.
Svar->address
Make-simple-svar
Address->svar: Turn an address into a variable name.
Svex-add-delay-top
Addr-scope: Scope for an address-p.