check-or-call-tests

other

(in-package "ACL2")

include-book

(include-book "check-or-call")

include-book

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

other

(assert-equal (mv-list 3 (check-or-call 'x)) '(nil nil nil))

other

(assert-equal (mv-list 3 (check-or-call ''4))
  '(nil nil nil))

other

(assert-equal (mv-list 3 (check-or-call ''t))
  '(nil nil nil))

other

(assert-equal (mv-list 3 (check-or-call ''nill))
  '(nil nil nil))

other

(assert-equal (mv-list 3 (check-or-call '(f x y)))
  '(nil nil nil))

other

(assert-equal (mv-list 3 (check-or-call '((lambda (x) (cons x x)) a)))
  '(nil nil nil))

other

(assert-equal (mv-list 3
    (check-or-call '(if a
        'nil
        b)))
  '(nil nil nil))

other

(assert-equal (mv-list 3
    (check-or-call '(if a
        b
        'nil)))
  '(nil nil nil))

other

(assert-equal (mv-list 3
    (check-or-call '(if a
        a
        b)))
  '(t a b))

other

(assert-equal (mv-list 3
    (check-or-call '(if a
        a
        (if b
          c
          d))))
  '(t a
    (if b
      c
      d)))

Included Books