		Search-engine friendly clone of the ACL2 documentation.

Pointed-integers

Def-pointed-integer-operations-loop

Events to generate the operations on pointed integers of give types.

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

Definitions and Theorems

Function: def-pointed-integer-operations-loop

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

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

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

Theorem: def-pointed-integer-operations-loop-of-type-list-fix-types

(defthm def-pointed-integer-operations-loop-of-type-list-fix-types
  (equal (def-pointed-integer-operations-loop (type-list-fix types))
         (def-pointed-integer-operations-loop types)))

Theorem: def-pointed-integer-operations-loop-type-list-equiv-congruence-on-types

(defthm
 def-pointed-integer-operations-loop-type-list-equiv-congruence-on-types
 (implies (type-list-equiv types types-equiv)
          (equal (def-pointed-integer-operations-loop types)
                 (def-pointed-integer-operations-loop types-equiv)))
 :rule-classes :congruence)