all-digit-charsp - ACL2 Book

other

(in-package "ACL2")

in-theory

(in-theory (disable digit-char-p))

all-digit-charspfunction

(defund all-digit-charsp
  (chars radix)
  (declare (xargs :guard (and (character-listp chars)
        (integerp radix)
        (<= 2 radix)
        (<= radix 36))))
  (if (endp chars)
    (null chars)
    (and (digit-char-p (first chars) radix)
      (all-digit-charsp (rest chars) radix))))