|
|
|---|
|
|
|
|---|
Raw constructor for honsed defmapping-infop structures.
Syntax:
(honsed-defmapping-info call$ expansion doma domb alpha beta
alpha-image beta-image beta-of-alpha
alpha-of-beta alpha-injective
beta-injective doma-guard domb-guard
alpha-guard beta-guard unconditional)This is identical to defmapping-info, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-defmapping-info (call$ expansion doma domb alpha beta alpha-image beta-image beta-of-alpha alpha-of-beta alpha-injective beta-injective doma-guard domb-guard alpha-guard beta-guard unconditional) (declare (xargs :guard (and (pseudo-event-formp call$) (pseudo-event-formp expansion) (pseudo-termfnp doma) (pseudo-termfnp domb) (pseudo-termfnp alpha) (pseudo-termfnp beta) (symbolp alpha-image) (symbolp beta-image) (symbolp beta-of-alpha) (symbolp alpha-of-beta) (symbolp alpha-injective) (symbolp beta-injective) (symbolp doma-guard) (symbolp domb-guard) (symbolp alpha-guard) (symbolp beta-guard) (booleanp unconditional)))) (mbe :logic (defmapping-info call$ expansion doma domb alpha beta alpha-image beta-image beta-of-alpha alpha-of-beta alpha-injective beta-injective doma-guard domb-guard alpha-guard beta-guard unconditional) :exec (hons (hons 'call$ call$) (hons (hons 'expansion expansion) (hons (hons 'doma doma) (hons (hons 'domb domb) (hons (hons 'alpha alpha) (hons (hons 'beta beta) (hons (hons 'alpha-image alpha-image) (hons (hons 'beta-image beta-image) (hons (hons 'beta-of-alpha beta-of-alpha) (hons (hons 'alpha-of-beta alpha-of-beta) (hons (hons 'alpha-injective alpha-injective) (hons (hons 'beta-injective beta-injective) (hons (hons 'doma-guard doma-guard) (hons (hons 'domb-guard domb-guard) (hons (hons 'alpha-guard alpha-guard) (hons (hons 'beta-guard beta-guard) (hons (hons 'unconditional unconditional) nil)))))))))))))))))))