Filtering...

check-user-lambda-tests

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

Included Books

check-user-lambda assert-bang assert-equal must-succeed-star
other
(in-package "ACL2")
include-book
(include-book "check-user-lambda")
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! (msgp (nth 0
      (mv-list 2 (check-user-lambda "(lambda (x) x)" (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2
        (check-user-lambda '(lambda (x) x . more) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2 (check-user-lambda '(lambda (x) x y) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2 (check-user-lambda '(lambda (x)) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2 (check-user-lambda '(lambdaa (x) x) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2 (check-user-lambda '(lambda "x" x) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2 (check-user-lambda '(lambda (x x) x) (w state))))))
other
(assert! (msgp (nth 0
      (mv-list 2
        (check-user-lambda '(lambda (x "y") x) (w state))))))
other
(assert-equal (mv-list 2 (check-user-lambda '(lambda (x) 3) (w state)))
  '((lambda (x) '3) (nil)))
other
(assert-equal (mv-list 2 (check-user-lambda '(lambda (x) x) (w state)))
  '((lambda (x) x) (nil)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (y) (len x)) (w state)))
  '((lambda (y) (len x)) (nil)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (x y) (mv x y z)) (w state)))
  '((lambda (x y) (cons x (cons y (cons z 'nil)))) (nil nil nil)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (state) state) (w state)))
  '((lambda (state) state) (state)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (state) (mv state 1)) (w state)))
  '((lambda (state) (cons state (cons '1 'nil))) (state nil)))
other
(must-succeed* (defstobj s)
  (assert-equal (mv-list 2
      (check-user-lambda '(lambda (state s) (mv s 0 state))
        (w state)))
    '((lambda (state s) (cons s (cons '0 (cons state 'nil)))) (s nil state))))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (x y) (+ x y)) (w state)))
  '((lambda (x y) (binary-+ x y)) (nil)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (z) (+ (len x) 55)) (w state)))
  '((lambda (z) (binary-+ (len x) '55)) (nil)))
other
(assert-equal (mv-list 2
    (check-user-lambda '(lambda (u)
        (let ((x 4))
          (+ x (len y))))
      (w state)))
  '((lambda (u) ((lambda (x y) (binary-+ x (len y))) '4 y)) (nil)))
other
(assert! (msgp (nth 0
      (mv-list 2
        (check-user-lambda '(lambda (x) (f x)) (w state))))))