Octal integer constant of type unsigned int.
Function: uint-oct-const
(defun uint-oct-const (x) (declare (xargs :guard (and (natp x) (uint-integerp x)))) (uint-from-integer x))
Theorem: uintp-of-uint-oct-const
(defthm uintp-of-uint-oct-const (uintp (uint-oct-const x)))