|
|
|---|
|
|
|
|---|
Raw constructor for honsed defbyte-infop structures.
Syntax:
(honsed-defbyte-info size signed)
This is identical to defbyte-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-defbyte-info (size signed) (declare (xargs :guard (and (or (posp size) (symbolp size) (and (acl2::tuplep 1 size) (symbolp (car size)))) (booleanp signed)))) (mbe :logic (defbyte-info size signed) :exec (hons (hons 'size size) (hons (hons 'signed signed) nil))))