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