		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 stobjp 
                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 stobjp
                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)
                             (booleanp stobjp)
                             (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 'stobjp stobjp)
        (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)))))))))))))))))))