|
|
|---|
|
|
|
|---|
Raw constructor for honsed vls-commandinfo-p structures.
Syntax:
(honsed-vls-commandinfo fn args type)
This is identical to vls-commandinfo, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-vls-commandinfo (fn args type) (declare (xargs :guard (and (symbolp fn) (symbol-listp args) (vls-commandtype-p type)))) (mbe :logic (vls-commandinfo fn args type) :exec (hons (hons 'fn fn) (hons (hons 'args args) (hons (hons 'type type) nil)))))