print-base-p - ACL2 Book

other

(in-package "ACL2")

print-base-p-forwardtheorem

(defthm print-base-p-forward
  (implies (print-base-p print-base)
    (and (integerp print-base)
      (<= 2 print-base)
      (<= print-base 16)))
  :rule-classes :forward-chaining :hints (("Goal" :in-theory (enable print-base-p))))