|
|
|---|
|
|
|
|---|
Raw constructor for honsed block$-p structures.
Syntax:
(honsed-block$ header transations ommer-headers)
This is identical to block$, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-block$ (header transations ommer-headers) (declare (xargs :guard (and (block-headerp header) (all-transactionp transations) (all-block-headerp ommer-headers)))) (mbe :logic (block$ header transations ommer-headers) :exec (hons (hons 'header header) (hons (hons 'transations transations) (hons (hons 'ommer-headers ommer-headers) nil)))))