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