Recognizer of values of type
(ullongp x) → yes/no
Function:
(defun ullongp (x) (declare (xargs :guard t)) (let ((__function__ 'ullongp)) (declare (ignorable __function__)) (and (consp x) (eq (car x) :ullong) (true-listp (cdr x)) (eql (len (cdr x)) 1) (b* ((get (std::da-nth 0 (cdr x)))) (ullong-integerp get)))))
Theorem:
(defthm booleanp-of-ullongp (b* ((yes/no (ullongp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm consp-when-ullongp (implies (ullongp x) (consp x)) :rule-classes :compound-recognizer)