string-listp

(in-package "ACL2")

(defsection std/typed-lists/string-listp
  :parents (std/typed-lists string-listp)
  :short "Lemmas about @(see string-listp) available in the @(see
std/typed-lists) library."
  :long "<p>Most of these are generated automatically with @(see
std::deflist).</p>"
  (deflist string-listp
    (x)
    (stringp x)
    :true-listp t
    :elementp-of-nil nil
    :already-definedp t
    :parents nil)
  (defthm true-listp-when-string-listp-rewrite
    (implies (string-listp x) (true-listp x))
    :rule-classes ((:rewrite :backchain-limit-lst 1)))
  (defthm string-listp-of-remove-equal
    (implies (string-listp x) (string-listp (remove-equal a x))))
  (defthm string-listp-of-remove-duplicates-equal
    (equal (string-listp (remove-duplicates-equal x))
      (string-listp (true-list-fix x)))))