		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%x.

Construct a hexadecimal-base direct numeric value notation element from a variable number of numbers.

The name of this macro is inspired by the ABNF notation %d<n1>.<n2>. ..., where <n1>, <n2>, ... are numbers in base 16: the name of this macro has the %x and the . of that notation.

Macro: %x.

(defmacro %x. (&rest numbers)
  (cons '%x.-fn
        (cons (cons 'list numbers) 'nil)))

Definitions and Theorems

Function: %x.-fn

(defun %x.-fn (nats)
  (declare (xargs :guard (nat-listp nats)))
  (element-num-val (num-val-direct (num-base-hex) nats)))

Theorem: elementp-of-%x.-fn

(defthm elementp-of-%x.-fn
  (b* ((element (%x.-fn nats)))
    (elementp element))
  :rule-classes :rewrite)

Theorem: %x.-fn-of-nat-list-fix-nats

(defthm %x.-fn-of-nat-list-fix-nats
  (equal (%x.-fn (nat-list-fix nats))
         (%x.-fn nats)))

Theorem: %x.-fn-nat-list-equiv-congruence-on-nats

(defthm %x.-fn-nat-list-equiv-congruence-on-nats
  (implies (acl2::nat-list-equiv nats nats-equiv)
           (equal (%x.-fn nats)
                  (%x.-fn nats-equiv)))
  :rule-classes :congruence)