Filtering...

fsublis-fn-tests

books/std/system/fsublis-fn-tests

Included Books

fsublis-fn assert-equal
other
(in-package "ACL2")
include-book
(include-book "fsublis-fn")
include-book
(include-book "std/testing/assert-equal" :dir :system)
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      ''#\c
      nil
      t))
  '(nil '#\c))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      ''#\c
      nil
      nil))
  '(nil '#\c))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      'y
      nil
      t))
  '(nil y))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      'y
      nil
      nil))
  '(nil y))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '(f (r x) y)
      nil
      t))
  '(nil (g (r x) y)))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '(f (r x) y)
      nil
      nil))
  '(nil (g (r x) y)))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '(h a)
      nil
      t))
  '(nil (cons a y)))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '(h a)
      nil
      nil))
  '((y) (h a)))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '((lambda (z w) (h (cons z w))) (f a) (j c))
      nil
      t))
  '(nil ((lambda (z w y) (cons (cons z w) y)) (g a) (j c) y)))
other
(assert-equal (mv-list 2
    (fsublis-fn-rec '((f . g) (h lambda (x) (cons x y)))
      '((lambda (z w) (h (cons z w))) (f a) (j c))
      nil
      nil))
  '((y) (h (cons z w))))
other
(assert-equal (mv-list 2
    (fsublis-fn '((f . g) (h lambda (x) (cons x y))) ''#\c nil))
  '(nil '#\c))
other
(assert-equal (mv-list 2
    (fsublis-fn '((f . g) (h lambda (x) (cons x y))) 'y nil))
  '(nil y))
other
(assert-equal (mv-list 2
    (fsublis-fn '((f . g) (h lambda (x) (cons x y)))
      '(f (r x) y)
      nil))
  '(nil (g (r x) y)))
other
(assert-equal (mv-list 2
    (fsublis-fn '((f . g) (h lambda (x) (cons x y))) '(h a) nil))
  '(nil (cons a y)))
other
(assert-equal (mv-list 2
    (fsublis-fn '((f . g) (h lambda (x) (cons x y)))
      '((lambda (z w) (h (cons z w))) (f a) (j c))
      nil))
  '(nil ((lambda (z w y) (cons (cons z w) y)) (g a) (j c) y)))
other
(assert-equal (fsublis-fn-simple '((f . g) (h . i)) '''(1 2 3))
  '''(1 2 3))
other
(assert-equal (fsublis-fn-simple '((f . g) (h . i)) 'xyz)
  'xyz)
other
(assert-equal (fsublis-fn-simple '((f . g) (h . i))
    '(f (cons (g (h a) b) c) d))
  '(g (cons (g (i a) b) c) d))
other
(assert-equal (fsublis-fn-simple '((f . g) (h . i))
    '(f ((lambda (x) (cons x (h 'a))) (g b))))
  '(g ((lambda (x) (cons x (i 'a))) (g b))))