		Search-engine friendly clone of the ACL2 documentation.

Addresses

Address

Fixtype of addresses.

This is a product type introduced by fty::defprod.

Fields

unwrap — any-p

To treat addresses abstractly, we define this fixtype as a wrapper of the fixtype of all ACL2 values. In other words, we can use any ACL2 value as an address, e.g. to construct examples and simulations.

Subtopics

Address-fix: Fixing function for address structures.
Addressp: Recognizer for address structures.
Address-equiv: Basic equivalence relation for address structures.
Make-address: Basic constructor macro for address structures.
Change-address: Modifying constructor for address structures.
Address->unwrap: Get the unwrap field from a address.