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