Event generated by defbyte-ihs-theorems.
(defbyte-ihs-theorems-fn type wrld) → event
Function:
(defun defbyte-ihs-theorems-fn (type wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'defbyte-ihs-theorems-fn)) (declare (ignorable __function__)) (b* (((unless (symbolp type)) (raise "The TYPE input must be a symbol, ~ but it is ~x0 instead." type)) (defbyte-table (table-alist *defbyte-table-name* wrld)) (defbyte-pair (assoc-eq type defbyte-table)) ((unless defbyte-pair) (raise "The TYPE input ~x0 must name a type ~ previously introduced via DEFBYTE, ~ but this is not the case." type)) (defbyte-info (cdr defbyte-pair)) (size (defbyte-info->size defbyte-info)) (signed (defbyte-info->signed defbyte-info)) (fty-table (get-fixtypes-alist wrld)) (fty-info (find-fixtype type fty-table)) (bytep (fixtype->pred fty-info)) (loghead/logext (if signed 'logext 'loghead)) (bytep-of-loghead/logext-of-size (acl2::packn-pos (list bytep '-of- loghead/logext '-of- size) bytep)) (x (intern-in-package-of-symbol "X" bytep)) (event (cons 'defrule (cons bytep-of-loghead/logext-of-size (cons (cons bytep (cons (cons loghead/logext (cons size (cons x 'nil))) 'nil)) (cons ':enable (cons bytep '(:prep-books ((include-book "arithmetic-5/top" :dir :system)))))))))) event)))