		Search-engine friendly clone of the ACL2 documentation.

Integer-ranges

Def-integer-range-loop

Events to generate fixtypes, functions, and theorems for ranges of integer types.

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

Definitions and Theorems

Function: def-integer-range-loop

(defun def-integer-range-loop (types)
  (declare (xargs :guard (type-listp types)))
  (declare (xargs :guard (type-nonchar-integer-listp types)))
  (cond ((endp types) nil)
        (t (cons (def-integer-range (car types))
                 (def-integer-range-loop (cdr types))))))

Theorem: pseudo-event-form-listp-of-def-integer-range-loop

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

Theorem: def-integer-range-loop-of-type-list-fix-types

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

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

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