|
|
|---|
|
|
|
|---|
Raw constructor for honsed expdata-surjmapp structures.
Syntax:
(honsed-expdata-surjmap surjname localp oldp
newp forth back forth-image back-image
back-of-forth forth-injective oldp-guard
newp-guard forth-guard back-guard hints)This is identical to expdata-surjmap, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-expdata-surjmap (surjname localp oldp newp forth back forth-image back-image back-of-forth forth-injective oldp-guard newp-guard forth-guard back-guard hints) (declare (xargs :guard (and (symbolp surjname) (booleanp localp) (pseudo-termfnp oldp) (pseudo-termfnp newp) (pseudo-termfnp forth) (pseudo-termfnp back) (symbolp forth-image) (symbolp back-image) (symbolp back-of-forth) (symbolp forth-injective) (symbolp oldp-guard) (symbolp newp-guard) (symbolp forth-guard) (symbolp back-guard) (keyword-value-listp hints)))) (mbe :logic (expdata-surjmap surjname localp oldp newp forth back forth-image back-image back-of-forth forth-injective oldp-guard newp-guard forth-guard back-guard hints) :exec (hons (hons 'surjname surjname) (hons (hons 'localp localp) (hons (hons 'oldp oldp) (hons (hons 'newp newp) (hons (hons 'forth forth) (hons (hons 'back back) (hons (hons 'forth-image forth-image) (hons (hons 'back-image back-image) (hons (hons 'back-of-forth back-of-forth) (hons (hons 'forth-injective forth-injective) (hons (hons 'oldp-guard oldp-guard) (hons (hons 'newp-guard newp-guard) (hons (hons 'forth-guard forth-guard) (hons (hons 'back-guard back-guard) (hons (hons 'hints hints) nil)))))))))))))))))