|
|
|---|
|
|
|
|---|
Raw constructor for expdata-surjmapp structures.
Syntax:
(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 the lowest-level constructor for expdata-surjmapp structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-expdata-surjmap or change-expdata-surjmap instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The expdata-surjmapp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-expdata-surjmap instead.
This is an ordinary constructor function introduced by std::defaggregate.
Function:
(defun 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)))) (cons (cons 'surjname surjname) (cons (cons 'localp localp) (cons (cons 'oldp oldp) (cons (cons 'newp newp) (cons (cons 'forth forth) (cons (cons 'back back) (cons (cons 'forth-image forth-image) (cons (cons 'back-image back-image) (cons (cons 'back-of-forth back-of-forth) (cons (cons 'forth-injective forth-injective) (cons (cons 'oldp-guard oldp-guard) (cons (cons 'newp-guard newp-guard) (cons (cons 'forth-guard forth-guard) (cons (cons 'back-guard back-guard) (cons (cons 'hints hints) nil))))))))))))))))