Filtering...

mvify-tests

books/std/system/mvify-tests

Included Books

mvify assert-equal
other
(in-package "ACL2")
include-book
(include-book "mvify")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (mvify '(cons x (cons y 'nil))) '(mv x y))
other
(assert-equal (mvify '(cons x (cons y (cons z (cons w 'nil)))))
  '(mv x y z w))
other
(assert-equal (mvify '(f a b)) '(f a b))
other
(assert-equal (mvify '(if a
      (f u)
      (g v)))
  '(if a
    (f u)
    (g v)))
other
(assert-equal (mvify '(if (cons x (cons y 'nil))
      (f u)
      (g v)))
  '(if (cons x (cons y 'nil))
    (f u)
    (g v)))
other
(assert-equal (mvify '(if a
      (cons x (cons y 'nil))
      (g v)))
  '(if a
    (mv x y)
    (g v)))
other
(assert-equal (mvify '(if a
      (f u)
      (cons x (cons y 'nil))))
  '(if a
    (f u)
    (mv x y)))
other
(assert-equal (mvify '(if a
      (cons x (cons y 'nil))
      (cons z (cons w 'nil))))
  '(if a
    (mv x y)
    (mv z w)))
other
(assert-equal (mvify '(return-last a (f u) (g v)))
  '(return-last a (f u) (g v)))
other
(assert-equal (mvify '(return-last (cons x (cons y 'nil)) (f u) (g v)))
  '(return-last (cons x (cons y 'nil)) (f u) (g v)))
other
(assert-equal (mvify '(return-last a (cons x (cons y 'nil)) (g v)))
  '(return-last a (mv x y) (g v)))
other
(assert-equal (mvify '(return-last a (f u) (cons x (cons y 'nil))))
  '(return-last a (f u) (mv x y)))
other
(assert-equal (mvify '(return-last a
      (cons x (cons y 'nil))
      (cons z (cons w 'nil))))
  '(return-last a (mv x y) (mv z w)))
other
(assert-equal (mvify '((lambda (a b) (f a b)) 'anything :anything))
  '((lambda (a b) (f a b)) 'anything :anything))
other
(assert-equal (mvify '((lambda (u) (cons x (cons y 'nil))) anything))
  '((lambda (u) (mv x y)) anything))
other
(assert-equal (mvify '((lambda (u)
       (if a
         (cons x (cons y (cons z 'nil)))
         (return-last a (h a) (cons u (cons v 'nil))))) '3/4))
  '((lambda (u)
     (if a
       (mv x y z)
       (return-last a (h a) (mv u v)))) '3/4))