Filtering...

one-way-unify-dollar-tests

books/std/system/one-way-unify-dollar-tests

Included Books

one-way-unify-dollar assert-equal
other
(in-package "ACL2")
include-book
(include-book "one-way-unify-dollar")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (mv-list 2 (one-way-unify$ 'x ''3 state))
  (list t (list (cons 'x ''3))))
other
(assert-equal (mv-list 2 (one-way-unify$ ''3 'x state))
  (list nil nil))
other
(assert-equal (mv-list 2 (one-way-unify$ '(f x '3) '(f '1 '3) state))
  (list t (list (cons 'x ''1))))