event-landmark-names-tests

Included Books

event-landmark-names assert-equal must-succeed-star

other

(in-package "ACL2")

include-book

(include-book "event-landmark-names")

include-book

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

include-book

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

other

(must-succeed* (defun f (x) x)
  (assert-equal (event-landmark-names (cddr (nth 0 (w state))))
    '(f)))

other

(must-succeed* (defun f (x) x)
  (verify-guards f)
  (assert-equal (event-landmark-names (cddr (nth 0 (w state))))
    nil))

other

(must-succeed* (mutual-recursion (defun f
      (term)
      (if (variablep term)
        0
        (if (fquotep term)
          0
          (1+ (f-lst (fargs term))))))
    (defun f-lst
      (terms)
      (if (endp terms)
        0
        (+ (f (car terms)) (f-lst (cdr terms))))))
  (assert-equal (event-landmark-names (cddr (nth 0 (w state))))
    '(f f-lst)))