Generate all the eight methods to write primitive arrays.
(atj-gen-shallow-primarray-write-methods) → methods
These methods are no longer generated, because ATJ's post-translation removes all their calls, and so there is no need for these methods to be generated. However, we keep this code around just in case for now.
Function:
(defun atj-gen-shallow-primarray-write-methods nil (declare (xargs :guard t)) (let ((__function__ 'atj-gen-shallow-primarray-write-methods)) (declare (ignorable __function__)) (list (atj-gen-shallow-primarray-write-method (primitive-type-boolean)) (atj-gen-shallow-primarray-write-method (primitive-type-char)) (atj-gen-shallow-primarray-write-method (primitive-type-byte)) (atj-gen-shallow-primarray-write-method (primitive-type-short)) (atj-gen-shallow-primarray-write-method (primitive-type-int)) (atj-gen-shallow-primarray-write-method (primitive-type-long)) (atj-gen-shallow-primarray-write-method (primitive-type-float)) (atj-gen-shallow-primarray-write-method (primitive-type-double)))))
Theorem:
(defthm jmethod-listp-of-atj-gen-shallow-primarray-write-methods (b* ((methods (atj-gen-shallow-primarray-write-methods))) (jmethod-listp methods)) :rule-classes :rewrite)