our-digit-char-p - ACL2 Book

other

(in-package "ACL2")

in-theory

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

our-digit-char-p-of-0-arg1theorem

(defthm our-digit-char-p-of-0-arg1
  (equal (our-digit-char-p #\0 radix)
    (if (< 0 radix)
      0
      nil))
  :hints (("Goal" :in-theory (enable our-digit-char-p))))