Top

Representation-of-integer-operations

Ullong-oct-const

Octal integer constant of type unsigned long long.

Definitions and Theorems

Function: ullong-oct-const

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

Theorem: ullongp-of-ullong-oct-const

(defthm ullongp-of-ullong-oct-const
  (ullongp (ullong-oct-const x)))