conjoin-equalities-tests

(in-package "ACL2")

(assert-equal (conjoin-equalities nil nil) *t*)

(assert-equal (conjoin-equalities (list 'lhs) (list 'rhs))
  '(equal lhs rhs))

(assert-equal (conjoin-equalities (list 'var ''#\c '(f a b))
    (list '((lambda (x) (cons x x)) '2)
      'xb
      '(h (j '3) (k x y z))))
  '(if (equal var ((lambda (x) (cons x x)) '2))
    (if (equal '#\c xb)
      (equal (f a b) (h (j '3) (k x y z)))
      'nil)
    'nil))