Basic constructor macro for command-error-malformed-value structures.
(make-command-error-malformed-value [:value <value>])
This is the usual way to construct command-error-malformed-value structures. It simply conses together a structure with the specified fields.
This macro generates a new command-error-malformed-value structure from scratch. See also change-command-error-malformed-value, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-command-error-malformed-value (&rest args) (std::make-aggregate 'command-error-malformed-value args '((:value)) 'make-command-error-malformed-value nil))
Function:
(defun command-error-malformed-value (value) (declare (xargs :guard (stringp value))) (declare (xargs :guard t)) (let ((__function__ 'command-error-malformed-value)) (declare (ignorable __function__)) (b* ((value (mbe :logic (acl2::str-fix value) :exec value))) (cons :malformed-value (list value)))))