Filtering...

defmapappend

books/std/util/tests/defmapappend
other
(in-package "STD")
other
(include-book "../defmapappend")
other
(include-book "../deflist")
other
(include-book "../defprojection")
other
(include-book "std/testing/assert-bang" :dir :system)
other
(deflist my-nat-listp
  (x)
  (natp x)
  :elementp-of-nil nil)
other
(defund nats
  (n)
  (declare (xargs :guard (natp n)))
  (if (zp n)
    nil
    (cons n (nats (- n 1)))))
other
(defthm my-nat-listp-of-nats
  (my-nat-listp (nats n))
  :hints (("Goal" :in-theory (enable nats))))
other
(defprojection map-nats
  (x)
  (nats x)
  :guard (my-nat-listp x)
  :optimize nil)
other
(defmapappend append-nats
  (x)
  (nats x)
  :guard (my-nat-listp x))
other
(value-triple (map-nats (nats 5)))
other
(value-triple (append-nats (nats 5)))
other
(defmapappend m0
  (x)
  (nats x)
  :guard (my-nat-listp x))
other
(assert! (let ((topic (find-topic 'm0
         (get-xdoc-table (w state)))))
    (not topic)))
other
(set-default-parents foo bar)
other
(defmapappend m1
  (x)
  (nats x)
  :guard (my-nat-listp x))
other
(assert! (let ((topic (find-topic 'm1
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic))
        '(foo bar)))))
other
(defmapappend m2
  (x)
  (nats x)
  :guard (my-nat-listp x)
  :parents (bar))
other
(assert! (let ((topic (find-topic 'm2
         (get-xdoc-table (w state)))))
    (and topic
      (equal (cdr (assoc :parents topic)) '(bar)))))
other
(defmapappend m3
  (x)
  (nats x)
  :guard (my-nat-listp x)
  :parents nil)
other
(assert! (let ((topic (find-topic 'm3
         (get-xdoc-table (w state)))))
    (not topic)))