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
(make employee :name "Jimmy"
:position "Unpaid Intern")
Creates a new employee structure with the given values for its
name, salary, and position fields. See defrec for more