assert-equal

(in-package "ACL2")

(defsection assert-equal
  :parents (std/testing errors)
  :short "Abbreviation for calling @(tsee assert!) on an equality."
  :long "@(def assert-equal)"
  (defmacro assert-equal (x y) `(assert! (equal ,X ,Y))))