Filtering...

remove-mbe-tests

books/std/system/remove-mbe-tests

Included Books

remove-mbe assert-equal
other
(in-package "ACL2")
include-book
(include-book "remove-mbe")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (remove-mbe-logic 'x) 'x)
other
(assert-equal (remove-mbe-logic ''0) ''0)
other
(assert-equal (remove-mbe-logic '(f x y z)) '(f x y z))
other
(assert-equal (remove-mbe-logic '((lambda (a b) (cons a b)) x '(1 2 3)))
  '((lambda (a b) (cons a b)) x '(1 2 3)))
other
(assert-equal (remove-mbe-logic '(return-last 'mbe1-raw (f x) (g y)))
  '(f x))
other
(assert-equal (remove-mbe-logic '(g x (return-last 'mbe1-raw a b)))
  '(g x a))
other
(assert-equal (remove-mbe-logic '(return-last 'mbe1-raw
      (return-last 'mbe1-raw a b)
      (return-last 'mbe1-raw c d)))
  'a)
other
(assert-equal (remove-mbe-logic '(f (return-last 'progn a b)))
  '(f (return-last 'progn a b)))
other
(assert-equal (remove-mbe-exec 'x) 'x)
other
(assert-equal (remove-mbe-exec ''0) ''0)
other
(assert-equal (remove-mbe-exec '(f x y z)) '(f x y z))
other
(assert-equal (remove-mbe-exec '((lambda (a b) (cons a b)) x '(1 2 3)))
  '((lambda (a b) (cons a b)) x '(1 2 3)))
other
(assert-equal (remove-mbe-exec '(return-last 'mbe1-raw (f x) (g y)))
  '(g y))
other
(assert-equal (remove-mbe-exec '(g x (return-last 'mbe1-raw a b)))
  '(g x b))
other
(assert-equal (remove-mbe-exec '(return-last 'mbe1-raw
      (return-last 'mbe1-raw a b)
      (return-last 'mbe1-raw c d)))
  'd)
other
(assert-equal (remove-mbe-exec '(f (return-last 'progn a b)))
  '(f (return-last 'progn a b)))