		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%b-

Construct a binary-base range numeric value notation element from a minimum and a maximum.

Signature
(%b- min max) → element
Arguments: min — Guard (natp min).; max — Guard (natp max).
Returns: element — Type (elementp element).

The name of this function is inspired by the ABNF notation %d<min>-<max>, where <min> and <max> are numbers in base 2: the name of this function has the %b and the - of that notation.

Definitions and Theorems

Function: %b-

(defun %b- (min max)
  (declare (xargs :guard (and (natp min) (natp max))))
  (element-num-val (num-val-range (num-base-bin) min max)))

Theorem: elementp-of-%b-

(defthm elementp-of-%b-
  (b* ((element (%b- min max)))
    (elementp element))
  :rule-classes :rewrite)

Theorem: %b--of-nfix-min

(defthm %b--of-nfix-min
  (equal (%b- (nfix min) max)
         (%b- min max)))

Theorem: %b--nat-equiv-congruence-on-min

(defthm %b--nat-equiv-congruence-on-min
  (implies (acl2::nat-equiv min min-equiv)
           (equal (%b- min max)
                  (%b- min-equiv max)))
  :rule-classes :congruence)

Theorem: %b--of-nfix-max

(defthm %b--of-nfix-max
  (equal (%b- min (nfix max))
         (%b- min max)))

Theorem: %b--nat-equiv-congruence-on-max

(defthm %b--nat-equiv-congruence-on-max
  (implies (acl2::nat-equiv max max-equiv)
           (equal (%b- min max)
                  (%b- min max-equiv)))
  :rule-classes :congruence)