Included Books
other
(in-package "ACL2")
include-book
(include-book "defchoose-queries")
include-book
(include-book "std/testing/assert-bang" :dir :system)
include-book
(include-book "std/testing/assert-equal" :dir :system)
include-book
(include-book "std/testing/must-succeed-star" :dir :system)
other
(must-succeed* (encapsulate (((f *) => *)) (local (defun f (x) x)) (defthm f-id (equal (f x) x))) (assert! (not (defchoosep 'f (w state)))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert! (defchoosep 'f (w state))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert! (defchoosep 'f (w state))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c)) :strengthen t) (assert! (defchoosep 'f (w state))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c)) :strengthen t) (assert! (defchoosep 'f (w state))))
other
(must-succeed* (encapsulate (((f *) => *)) (local (defun f (x) x)) (defthm f-id (equal (f x) x))) (assert! (not (defchoose-namep 'f (w state)))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert! (defchoose-namep 'f (w state))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert! (defchoose-namep 'f (w state))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c)) :strengthen t) (assert! (defchoose-namep 'f (w state))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c)) :strengthen t) (assert! (defchoose-namep 'f (w state))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert-equal (defchoose-bound-vars 'f (w state)) '(x)))
other
(must-succeed* (defchoose f (x) (a b c) (equal x (list a b c))) (assert-equal (defchoose-bound-vars 'f (w state)) '(x)))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert-equal (defchoose-bound-vars 'f (w state)) '(x y)))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c)) :strengthen t) (assert-equal (defchoose-bound-vars 'f (w state)) '(x)))
other
(must-succeed* (defchoose f (x) (a b c) (equal x (list a b c)) :strengthen t) (assert-equal (defchoose-bound-vars 'f (w state)) '(x)))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c)) :strengthen t) (assert-equal (defchoose-bound-vars 'f (w state)) '(x y)))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert! (not (defchoose-strengthen 'f (w state)))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert! (not (defchoose-strengthen 'f (w state)))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c)) :strengthen t) (assert! (defchoose-strengthen 'f (w state))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c)) :strengthen t) (assert! (defchoose-strengthen 'f (w state))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert-equal (defchoose-untrans-body 'f (w state)) '(equal x (list a b c))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert-equal (defchoose-untrans-body 'f (w state)) '(equal (cons x y) (list a b c))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c)) :strengthen t) (assert-equal (defchoose-untrans-body 'f (w state)) '(equal x (list a b c))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c)) :strengthen t) (assert-equal (defchoose-untrans-body 'f (w state)) '(equal (cons x y) (list a b c))))
other
(must-succeed* (defchoose f x (a b c) (equal x (list a b c))) (assert-equal (defchoose-body 'f (w state)) '(equal x (cons a (cons b (cons c 'nil))))))
other
(must-succeed* (defchoose f (x y) (a b c) (equal (cons x y) (list a b c))) (assert-equal (defchoose-body 'f (w state)) '(equal (cons x y) (cons a (cons b (cons c 'nil))))))