Top

Representation-of-integer-operations

Ulong-hex-const

Hexadecimal integer constant of type unsigned long.

Definitions and Theorems

Function: ulong-hex-const

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

Theorem: ulongp-of-ulong-hex-const

(defthm ulongp-of-ulong-hex-const
  (ulongp (ulong-hex-const x)))