Top

Representation-of-integer-operations

Slong-dec-const

Decimal integer constant of type signed long.

Definitions and Theorems

Function: slong-dec-const

(defun slong-dec-const (x)
  (declare (xargs :guard (and (natp x) (slong-integerp x))))
  (slong-from-integer x))

Theorem: slongp-of-slong-dec-const

(defthm slongp-of-slong-dec-const
  (slongp (slong-dec-const x)))