		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%x-

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

Signature
(%x- 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 %x<min>-<max>, where <min> and <max> are numbers in base 16: the name of this function has the %x and the - of that notation.

Definitions and Theorems

Function: %x-

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

Theorem: elementp-of-%x-

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

Theorem: %x--of-nfix-min

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

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

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

Theorem: %x--of-nfix-max

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

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

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