|
|
|---|
|
|
|
|---|
Raw constructor for honsed isodata-isomapp structures.
Syntax:
(honsed-isodata-isomap isoname localp oldp newp forth back
forth-image back-image back-of-forth
forth-of-back forth-injective
back-injective oldp-guard
newp-guard forth-guard back-guard hints)This is identical to isodata-isomap, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-isodata-isomap (isoname localp oldp newp forth back forth-image back-image back-of-forth forth-of-back forth-injective back-injective oldp-guard newp-guard forth-guard back-guard hints) (declare (xargs :guard (and (symbolp isoname) (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-of-back) (symbolp forth-injective) (symbolp back-injective) (symbolp oldp-guard) (symbolp newp-guard) (symbolp forth-guard) (symbolp back-guard) (keyword-value-listp hints)))) (mbe :logic (isodata-isomap isoname localp oldp newp forth back forth-image back-image back-of-forth forth-of-back forth-injective back-injective oldp-guard newp-guard forth-guard back-guard hints) :exec (hons (hons 'isoname isoname) (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-of-back forth-of-back) (hons (hons 'forth-injective forth-injective) (hons (hons 'back-injective back-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)))))))))))))))))))