		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%b.-fn

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

Definitions and Theorems

Function: %b.-fn

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

Theorem: elementp-of-%b.-fn

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

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

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

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

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