Generate the fixtype of the structures defined by the defstruct.
(defstruct-gen-fixtype struct-tag struct-tag-p struct-tag-fix struct-tag-equiv) → event
Function:
(defun defstruct-gen-fixtype (struct-tag struct-tag-p struct-tag-fix struct-tag-equiv) (declare (xargs :guard (and (symbolp struct-tag) (symbolp struct-tag-p) (symbolp struct-tag-fix) (symbolp struct-tag-equiv)))) (let ((__function__ 'defstruct-gen-fixtype)) (declare (ignorable __function__)) (cons 'fty::deffixtype (cons struct-tag (cons ':pred (cons struct-tag-p (cons ':fix (cons struct-tag-fix (cons ':equiv (cons struct-tag-equiv '(:define t :forward t)))))))))))
Theorem:
(defthm pseudo-event-formp-of-defstruct-gen-fixtype (b* ((event (defstruct-gen-fixtype struct-tag struct-tag-p struct-tag-fix struct-tag-equiv))) (pseudo-event-formp event)) :rule-classes :rewrite)