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