Filtering...

pseudo-event-form-listp

books/system/pseudo-event-form-listp

Included Books

pseudo-event-formp
other
(in-package "ACL2")
include-book
(include-book "pseudo-event-formp")
other
(defsection pseudo-event-form-listp
  :parents (system-utilities-non-built-in)
  :short "Recognize true lists of well-formed event forms."
  (defun pseudo-event-form-listp
    (x)
    (declare (xargs :guard t))
    (if (atom x)
      (equal x nil)
      (and (pseudo-event-formp (car x))
        (pseudo-event-form-listp (cdr x))))))