|
|
|---|
|
|
|
|---|
Raw constructor for honsed evmac-appcondp structures.
Syntax:
(honsed-evmac-appcond name formula)
This is identical to evmac-appcond, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-evmac-appcond (name formula) (declare (xargs :guard (and (keywordp name) (pseudo-termp formula)))) (mbe :logic (evmac-appcond name formula) :exec (hons (hons 'name name) (hons (hons 'formula formula) nil))))