		Search-engine friendly clone of the ACL2 documentation.

Isodata-isomapp

Isodata-isomap

Raw constructor for isodata-isomapp structures.

Syntax:

(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 the lowest-level constructor for isodata-isomapp structures. It simply conses together a structure with the specified fields.

Note: It's generally better to use macros like make-isodata-isomap or change-isodata-isomap instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.

The isodata-isomapp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-isodata-isomap instead.

Definition

This is an ordinary constructor function introduced by std::defaggregate.

Function: isodata-isomap

(defun 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))))
 (cons
  (cons 'isoname isoname)
  (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-of-back forth-of-back)
           (cons
            (cons 'forth-injective forth-injective)
            (cons
               (cons 'back-injective back-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))))))))))))))))))