Map a decimal, octal, or hexadecimal constant to a value and to an integer constant base in the language definition.
(ldm-dec/oct/hex-const const) → (mv value base)
Function:
(defun ldm-dec/oct/hex-const (const) (declare (xargs :guard (dec/oct/hex-constp const))) (let ((__function__ 'ldm-dec/oct/hex-const)) (declare (ignorable __function__)) (dec/oct/hex-const-case const :dec (mv const.value (c::iconst-base-dec)) :oct (mv const.value (c::iconst-base-oct)) :hex (mv (str::hex-digit-chars-value const.digits) (c::iconst-base-hex)))))
Theorem:
(defthm natp-of-ldm-dec/oct/hex-const.value (b* (((mv acl2::?value ?base) (ldm-dec/oct/hex-const const))) (natp value)) :rule-classes :rewrite)
Theorem:
(defthm iconst-basep-of-ldm-dec/oct/hex-const.base (b* (((mv acl2::?value ?base) (ldm-dec/oct/hex-const const))) (c::iconst-basep base)) :rule-classes :rewrite)
Theorem:
(defthm ldm-dec/oct/hex-const-of-dec/oct/hex-const-fix-const (equal (ldm-dec/oct/hex-const (dec/oct/hex-const-fix const)) (ldm-dec/oct/hex-const const)))
Theorem:
(defthm ldm-dec/oct/hex-const-dec/oct/hex-const-equiv-congruence-on-const (implies (dec/oct/hex-const-equiv const const-equiv) (equal (ldm-dec/oct/hex-const const) (ldm-dec/oct/hex-const const-equiv))) :rule-classes :congruence)