Top

Representation-of-integer-operations

Ulong-oct-const

Octal integer constant of type unsigned long.

Definitions and Theorems

Function: ulong-oct-const

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

Theorem: ulongp-of-ulong-oct-const

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