		Search-engine friendly clone of the ACL2 documentation.

Pointed-integers

Uchar-write

Representation of a write of a pointed type unsigned char.

Signature
(uchar-write x) → x
Arguments: x — Guard (ucharp x).
Returns: x — Type (star (ucharp x)).

Definitions and Theorems

Function: uchar-write

(defun uchar-write (x)
  (declare (xargs :guard (ucharp x)))
  (let ((__function__ 'uchar-write))
    (declare (ignorable __function__))
    (uchar-fix x)))

Theorem: return-type-of-uchar-write

(defthm return-type-of-uchar-write
  (b* ((x (uchar-write x)))
    (star (ucharp x)))
  :rule-classes :rewrite)

Theorem: ucharp-of-uchar-write

(defthm ucharp-of-uchar-write
  (b* ((x (uchar-write x))) (ucharp x))
  :rule-classes :rewrite)

Theorem: uchar-write-of-uchar-fix-x

(defthm uchar-write-of-uchar-fix-x
  (equal (uchar-write (uchar-fix x))
         (uchar-write x)))

Theorem: uchar-write-uchar-equiv-congruence-on-x

(defthm uchar-write-uchar-equiv-congruence-on-x
  (implies (uchar-equiv x x-equiv)
           (equal (uchar-write x)
                  (uchar-write x-equiv)))
  :rule-classes :congruence)