pseudo-command-landmark-listp-tests

Included Books

pseudo-command-landmark-listp assert-bang must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "pseudo-command-landmark-listp")

include-book

(include-book "std/testing/assert-bang" :dir :system)

include-book

(include-book "std/testing/must-succeed-star" :dir :system)

other

(must-succeed* (defun latest-command-landmark
    (wrld)
    (declare (xargs :guard (plist-worldp wrld)))
    (if (endp wrld)
      nil
      (let ((triple (car wrld)))
        (if (eq (car triple) 'command-landmark)
          (cddr triple)
          (latest-command-landmark (cdr wrld))))))
  (comp t)
  (assert! (pseudo-command-landmark-listp (list (latest-command-landmark (w state))))))