		Search-engine friendly clone of the ACL2 documentation.

Defmapping-infop

Defmapping-info

Raw constructor for defmapping-infop structures.

Syntax:

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

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

The defmapping-infop structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-defmapping-info instead.

Definition

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

Function: defmapping-info

(defun 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))))
 (cons
  (cons 'call$ call$)
  (cons
   (cons 'expansion expansion)
   (cons
    (cons 'doma doma)
    (cons
     (cons 'domb domb)
     (cons
      (cons 'alpha alpha)
      (cons
       (cons 'beta beta)
       (cons
        (cons 'alpha-image alpha-image)
        (cons
         (cons 'beta-image beta-image)
         (cons
          (cons 'beta-of-alpha beta-of-alpha)
          (cons
           (cons 'alpha-of-beta alpha-of-beta)
           (cons
            (cons 'alpha-injective alpha-injective)
            (cons
             (cons 'beta-injective beta-injective)
             (cons
              (cons 'doma-guard doma-guard)
              (cons
               (cons 'domb-guard domb-guard)
               (cons (cons 'alpha-guard alpha-guard)
                     (cons (cons 'beta-guard beta-guard)
                           (cons (cons 'unconditional unconditional)
                                 nil))))))))))))))))))