|
|
|---|
|
|
|
|---|
Raw constructor for honsed stvdata-p structures.
Syntax:
(honsed-stvdata inputs outputs internals overrides)
This is identical to stvdata, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-stvdata (inputs outputs internals overrides) (declare (xargs :guard (and (true-list-listp inputs) (true-list-listp outputs) (true-list-listp internals) (true-list-listp overrides)))) (mbe :logic (stvdata inputs outputs internals overrides) :exec (hons :stvdata (hons (hons 'inputs inputs) (hons (hons 'outputs outputs) (hons (hons 'internals internals) (hons (hons 'overrides overrides) nil)))))))