defredundant-tests

(in-package "STD")

(include-book "defredundant")

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

(assert! (equal (let ((world (w state)))
      (find-macro-aliases-for-defun (access-event-tuple-form (get-event-tuple 'binary-append world))
        world))
    '(append)))

(assert! (b* ((world (w state)) ((mv macros fns) (find-defun-aliases-for-macro (access-event-tuple-form (get-event-tuple 'append world))
          world)))
    (and (equal macros '(append))
      (equal fns '(binary-append)))))