		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%b.

Construct a binary-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 2: the name of this macro has the %b and the . of that notation.

Macro: %b.

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

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)