Access
Accessor macro for defrec structures.
The access macro is built into ACL2, and allows you to access
particular fields from structures that have been introduced with defrec. For instance:
(access employee x :name)
would return the name field from the employee x. See defrec for more information.
