		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%x.-fn

Signature
(%x.-fn nats) → element
Arguments: nats — Guard (nat-listp nats).
Returns: element — Type (elementp element).

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)