		Search-engine friendly clone of the ACL2 documentation.

Pointed-integers

Ullong-read

Representation of a read of a pointed type unsigned long long.

Signature
(ullong-read x) → x
Arguments: x — Guard (star (ullongp x)).
Returns: x — Type (ullongp x).

Definitions and Theorems

Function: ullong-read

(defun ullong-read (x)
  (declare (xargs :guard (star (ullongp x))))
  (let ((__function__ 'ullong-read))
    (declare (ignorable __function__))
    (ullong-fix x)))

Theorem: ullongp-of-ullong-read

(defthm ullongp-of-ullong-read
  (b* ((x (ullong-read x))) (ullongp x))
  :rule-classes :rewrite)