Basic constructor macro for vl-coredatatype-info structures.
(make-vl-coredatatype-info [:coretypename <coretypename>] [:keyword <keyword>] [:default-signedp <default-signedp>] [:takes-signingp <takes-signingp>] [:takes-dimensionsp <takes-dimensionsp>] [:4valuedp <4valuedp>] [:size <size>])
This is the usual way to construct vl-coredatatype-info structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-coredatatype-info structure from scratch. See also change-vl-coredatatype-info, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-coredatatype-info (&rest args) (std::make-aggregate 'vl-coredatatype-info args '((:coretypename) (:keyword) (:default-signedp) (:takes-signingp) (:takes-dimensionsp) (:4valuedp) (:size)) 'make-vl-coredatatype-info nil))
Function:
(defun vl-coredatatype-info (coretypename keyword default-signedp takes-signingp takes-dimensionsp 4valuedp size) (declare (xargs :guard (and (vl-coretypename-p coretypename) (symbolp keyword) (booleanp default-signedp) (booleanp takes-signingp) (booleanp takes-dimensionsp) (booleanp 4valuedp) (maybe-natp size)))) (declare (xargs :guard t)) (let ((__function__ 'vl-coredatatype-info)) (declare (ignorable __function__)) (b* ((coretypename (mbe :logic (vl-coretypename-fix coretypename) :exec coretypename)) (keyword (mbe :logic (acl2::symbol-fix keyword) :exec keyword)) (default-signedp (mbe :logic (acl2::bool-fix default-signedp) :exec default-signedp)) (takes-signingp (mbe :logic (acl2::bool-fix takes-signingp) :exec takes-signingp)) (takes-dimensionsp (mbe :logic (acl2::bool-fix takes-dimensionsp) :exec takes-dimensionsp)) (4valuedp (mbe :logic (acl2::bool-fix 4valuedp) :exec 4valuedp)) (size (mbe :logic (maybe-natp-fix size) :exec size))) (std::prod-cons (std::prod-cons coretypename (std::prod-cons keyword default-signedp)) (std::prod-cons (std::prod-cons takes-signingp takes-dimensionsp) (std::prod-cons 4valuedp size))))))