boolean-listp

(in-package "ACL2")

(defsection std/typed-lists/boolean-listp
  :parents (std/typed-lists boolean-listp)
  :short "Lemmas about @(see boolean-listp) available in the @(see
std/typed-lists) library."
  :long "<p>Most of these are generated automatically with @(see
std::deflist).</p>"
  (deflist boolean-listp
    (x)
    (booleanp x)
    :true-listp t
    :elementp-of-nil t
    :already-definedp t
    :parents nil
    :verbosep t
    :theory-hack ((local (in-theory (enable booleanp boolean-listp)))))
  (in-theory (disable boolean-listp-of-cons))
  (defthm boolean-listp-of-remove-equal
    (implies (boolean-listp x)
      (boolean-listp (remove-equal a x))))
  (defthm boolean-listp-of-make-list-ac
    (equal (boolean-listp (make-list-ac n x ac))
      (and (boolean-listp ac) (or (booleanp x) (zp n)))))
  (defthm eqable-listp-when-boolean-listp
    (implies (boolean-listp x) (eqlable-listp x)))
  (defthm symbol-listp-when-boolean-listp
    (implies (boolean-listp x) (symbol-listp x))))