rational-listp

(in-package "ACL2")

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