(atj-type-to-pred-gen-mono-thms) → *
Function:
(defun atj-type-to-pred-gen-mono-thms nil (declare (xargs :guard t)) (let ((__function__ 'atj-type-to-pred-gen-mono-thms)) (declare (ignorable __function__)) (b* ((types (list (atj-type-acl2 (atj-atype-integer)) (atj-type-acl2 (atj-atype-rational)) (atj-type-acl2 (atj-atype-number)) (atj-type-acl2 (atj-atype-character)) (atj-type-acl2 (atj-atype-string)) (atj-type-acl2 (atj-atype-symbol)) (atj-type-acl2 (atj-atype-boolean)) (atj-type-acl2 (atj-atype-cons)) (atj-type-acl2 (atj-atype-value)) (atj-type-jprim (primitive-type-boolean)) (atj-type-jprim (primitive-type-char)) (atj-type-jprim (primitive-type-byte)) (atj-type-jprim (primitive-type-short)) (atj-type-jprim (primitive-type-int)) (atj-type-jprim (primitive-type-long)) (atj-type-jprim (primitive-type-float)) (atj-type-jprim (primitive-type-double)) (atj-type-jprimarr (primitive-type-boolean)) (atj-type-jprimarr (primitive-type-char)) (atj-type-jprimarr (primitive-type-byte)) (atj-type-jprimarr (primitive-type-short)) (atj-type-jprimarr (primitive-type-int)) (atj-type-jprimarr (primitive-type-long)) (atj-type-jprimarr (primitive-type-float)) (atj-type-jprimarr (primitive-type-double))))) (cons 'encapsulate (cons 'nil (cons '(set-ignore-ok t) (atj-type-to-pred-gen-mono-thms-2 types types)))))))