Make
Constructor macro for defrec structures.
The make macro is built into ACL2, and allows you to construct
new instances of structures that have been introduced with defrec. For
instance:
(make employee :name "Jimmy"
:salary 0
:position "Unpaid Intern")
Creates a new employee structure with the given values for its
name, salary, and position fields. See defrec for more
information.
