		Search-engine friendly clone of the ACL2 documentation.

Representation-of-integer-operations

Def-integer-operations-2-loop-same

Events to generate the ACL2 models of the C integer operations that involve two identical integer types from a list.

Signature
(def-integer-operations-2-loop-same types) → events
Arguments: types — Guard (type-listp types).
Returns: events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: def-integer-operations-2-loop-same

(defun def-integer-operations-2-loop-same (types)
 (declare (xargs :guard (type-listp types)))
 (declare (xargs :guard (type-nonchar-integer-listp types)))
 (let ((__function__ 'def-integer-operations-2-loop-same))
  (declare (ignorable __function__))
  (cond
      ((endp types) nil)
      (t (cons (def-integer-operations-2 (car types)
                                         (car types))
               (def-integer-operations-2-loop-same (cdr types)))))))

Theorem: pseudo-event-form-listp-of-def-integer-operations-2-loop-same

(defthm
      pseudo-event-form-listp-of-def-integer-operations-2-loop-same
  (b* ((events (def-integer-operations-2-loop-same types)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)