Octal integer constant of type signed long long.
Function: sllong-oct-const
(defun sllong-oct-const (x) (declare (xargs :guard (and (natp x) (sllong-integerp x)))) (sllong-from-integer x))
Theorem: sllongp-of-sllong-oct-const
(defthm sllongp-of-sllong-oct-const (sllongp (sllong-oct-const x)))