Filtering...

defval

books/std/util/tests/defval

Included Books

defval assert-bang
other
(in-package "ACL2")
include-book
(include-book "../defval")
include-book
(include-book "std/testing/assert-bang" :dir :system)
other
(defxdoc test-par1 :parents (defval))
other
(defxdoc test-par2 :parents (defval))
other
(defval *parent-test1*
  :parents (test-par1)
  :short "test1 short"
  :long "<p>test1 long</p>"
  :showdef t
  :showval t
  (make-list 10))
other
(defval *parent-test2*
  :showdef nil
  :showval nil
  (make-list 100))
local
(local (set-default-parents (test-par2)))
other
(defval *parent-test3* :showval t (make-list 123))
other
(assert! (b* ((topic (find-topic '*parent-test1*
         (get-xdoc-table (w state)))) (parents (cdr (assoc :parents topic))))
    (equal parents '(test-par1))))
other
(assert! (b* ((topic (find-topic '*parent-test2*
         (get-xdoc-table (w state)))) (parents (cdr (assoc :parents topic))))
    (equal parents '(undocumented))))
other
(assert! (b* ((topic (find-topic '*parent-test3*
         (get-xdoc-table (w state)))) (parents (cdr (assoc :parents topic))))
    (equal parents '(test-par2))))
other
(assert! (equal *parent-test1* (make-list 10)))
other
(assert! (equal *parent-test2* (make-list 100)))
other
(assert! (equal *parent-test3* (make-list 123)))
other
(defval *demo1* (make-list 100))
other
(defval *demo2* :showdef t :showval nil (make-list 100))
other
(defval *demo3* :showdef t :showval t (make-list 100))
other
(defval *demo4* :showdef nil :showval t (make-list 100))
other
(defval *demo5* :showdef nil :showval nil (make-list 100))
other
(assert! (equal *demo1* (make-list 100)))
other
(assert! (equal *demo2* (make-list 100)))
other
(assert! (equal *demo3* (make-list 100)))
other
(assert! (equal *demo4* (make-list 100)))
other
(assert! (equal *demo5* (make-list 100)))
other
(defval *test-kwd* :foo)
other
(assert! (equal *test-kwd* :foo))
other
(defval *test-int* 3)
other
(assert! (equal *test-int* 3))
other
(defval *test-kwd2*
  :foo :parents (parent-test1)
  :short "Blah")
other
(defval *test-kwd3*
  :parents (parent-test1)
  :foo :short "Blah")
other
(defval *test-kwd4*
  :parents (parent-test1)
  :short "Blah"
  :foo)
other
(assert! (equal *test-kwd2* :foo))
other
(assert! (equal *test-kwd3* :foo))
other
(assert! (equal *test-kwd4* :foo))
other
(defval *test-kwd5* :short)
other
(assert! (equal *test-kwd5* :short))
other
(defval *event-test1*
  17
  ///
  (defthm int-of-event-test1
    (integerp *event-test1*)
    :rule-classes nil))
other
(defval *event-test2*
  :foo ///
  (defthm keywordp-event-test2
    (keywordp *event-test2*)
    :rule-classes nil))
other
(assert! (equal *test-kwd5* :short))
fibfunction
(defun fib
  (n)
  (declare (xargs :guard (natp n)))
  (cond ((zp n) 1)
    ((eql n 1) 1)
    (t (+ (fib (- n 1)) (fib (- n 2))))))
other
(defval *defval-example-number*
  :parents (defval)
  :short "Example of a constant for @(see defval)."
  :long "<p>This number is not very important.</p>"
  (fib 5))
other
(assert! (equal *defval-example-number* (fib 5)))