Aggregate and ftyps " p" help - acl2/acl2 GitHub Wiki

This may belong in a :doc topic, but just putting it here is easier for now.

(1:38:01 PM) clop: it's a little trickier than defaggregate
(1:38:25 PM) clop: (defaggregate foo ...) automatically adds a -p to the recognizer
(1:38:29 PM) clop: and defprod does the same
(1:38:41 PM) clop: but defprod lets you drop the -p on fields, e.g.
(1:39:13 PM) clop: where you might write (mod vl-module-p) as the field of a defaggregate
(1:39:21 PM) clop: you can write either (mod vl-module) or (mod vl-module-p)