Defaggrify-defrec
Add defaggregate-style emulation for defrec records.
The defrec macro is an undocumented utility which is used
within the ACL2 theorem prover to introduce structures. Although many of the
details are different, it is in many ways like defaggregate.
(defaggrify-defrec rec) is a macro that automatically adds
defaggregate-style accessors and b* binders that work on
defrec structures.
Typical usage is, e.g.,:
(in-package "ACL2")
(std::defaggrify-defrec rewrite-rule)
(std::defaggrify-defrec def-body)
...
We may eventually extend this to include additional defaggregate-style
features such as make- and change- macros.
