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