Filtering...

check-user-term-tests

books/std/system/check-user-term-tests

Included Books

check-user-term assert-bang assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "check-user-term")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(assert-equal (mv-list 2 (check-user-term 3 (w state)))
  '('3 (nil)))
other
(assert-equal (mv-list 2 (check-user-term 'x (w state)))
  '(x (nil)))
other
(assert-equal (mv-list 2 (check-user-term '(len x) (w state)))
  '((len x) (nil)))
other
(assert-equal (mv-list 2 (check-user-term '(mv x y z) (w state)))
  '((cons x (cons y (cons z 'nil))) (nil nil nil)))
other
(assert-equal (mv-list 2 (check-user-term 'state (w state)))
  '(state (state)))
other
(assert-equal (mv-list 2 (check-user-term '(mv state 1) (w state)))
  '((cons state (cons '1 'nil)) (state nil)))
other
(must-succeed* (defstobj s)
  (assert-equal (mv-list 2 (check-user-term '(mv s 0 state) (w state)))
    '((cons s (cons '0 (cons state 'nil))) (s nil state))))
other
(assert-equal (mv-list 2 (check-user-term '(+ x y) (w state)))
  '((binary-+ x y) (nil)))
other
(assert-equal (mv-list 2 (check-user-term '(+ (len x) 55) (w state)))
  '((binary-+ (len x) '55) (nil)))
other
(assert-equal (mv-list 2
    (check-user-term '(let ((x 4))
        (+ x (len y)))
      (w state)))
  '(((lambda (x y) (binary-+ x (len y))) '4 y) (nil)))
other
(assert! (msgp (nth 0 (mv-list 2 (check-user-term '(f x) (w state))))))