Filtering...

pseudo-tests-and-call-listp

books/std/system/pseudo-tests-and-call-listp

Included Books

other
(in-package "ACL2")
include-book
(include-book "pseudo-tests-and-callp")
include-book
(include-book "std/util/deflist" :dir :system)
other
(deflist pseudo-tests-and-call-listp
  (x)
  :parents (std/system)
  :short "Recognize true lists of well-formed @('tests-and-call') records."
  (pseudo-tests-and-callp x)
  :true-listp t
  :elementp-of-nil nil)