Top

Representation-of-integer-operations

Uint-hex-const

Hexadecimal integer constant of type unsigned int.

Definitions and Theorems

Function: uint-hex-const

(defun uint-hex-const (x)
  (declare (xargs :guard (and (natp x) (uint-integerp x))))
  (uint-from-integer x))

Theorem: uintp-of-uint-hex-const

(defthm uintp-of-uint-hex-const
  (uintp (uint-hex-const x)))