		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

%d-

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

Signature
(%d- 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 10: the name of this function has the %d and the - of that notation.

Definitions and Theorems

Function: %d-

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

Theorem: elementp-of-%d-

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

Theorem: %d--of-nfix-min

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

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

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

Theorem: %d--of-nfix-max

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

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

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