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