Filtering...

stobjtab

books/std/stobjs/stobjtab

Included Books

stobj-table absstobjs
other
(in-package "ACL2")
include-book
(include-book "stobj-table")
include-book
(include-book "absstobjs")
stobjtab$apfunction
(defun stobjtab$ap
  (stobjtab$a)
  (declare (xargs :guard t)
    (ignorable stobjtab$a))
  t)
create-stobjtab$afunction
(defun create-stobjtab$a nil (declare (xargs :guard t)) nil)
stbl-get$afunction
(defun stbl-get$a
  (k stobjtab$a default)
  (declare (xargs :guard t))
  (let ((pair (hons-assoc-equal k stobjtab$a)))
    (if pair
      (cdr pair)
      default)))
stbl-put$afunction
(defun stbl-put$a
  (k v stobjtab$a)
  (declare (xargs :guard t))
  (cons (cons k v) stobjtab$a))
stbl-boundp$afunction
(defun stbl-boundp$a
  (k stobjtab$a)
  (declare (xargs :guard t))
  (consp (hons-assoc-equal k stobjtab$a)))
stbl-rem$afunction
(defun stbl-rem$a
  (k stobjtab$a)
  (declare (xargs :guard t))
  (hons-remove-assoc k stobjtab$a))
stbl-count$afunction
(defun stbl-count$a
  (stobjtab$a)
  (declare (xargs :guard t))
  (count-keys stobjtab$a))
stbl-clear$afunction
(defun stbl-clear$a
  (stobjtab$a)
  (declare (xargs :guard t)
    (ignorable stobjtab$a))
  nil)
stbl-init$afunction
(defun stbl-init$a
  (ht-size rehash-size rehash-threshold stobjtab$a)
  (declare (xargs :guard (and (or (natp ht-size) (not ht-size))
        (or (and (rationalp rehash-size) (<= 1 rehash-size))
          (not rehash-size))
        (or (and (rationalp rehash-threshold)
            (<= 0 rehash-threshold)
            (<= rehash-threshold 1))
          (not rehash-threshold))))
    (ignorable ht-size rehash-size rehash-threshold stobjtab$a))
  nil)
other
(defun-nx stbl-corr
  (stobj-table stobjtab$a)
  (equal stobj-table (list stobjtab$a)))
local
(local (in-theory (enable nth update-nth)))
other
(defabsstobj-events stobjtab
  :foundation stobj-table
  :recognizer (stobjtabp :logic stobjtab$ap :exec stobj-tablep)
  :creator (create-stobjtab :logic create-stobjtab$a
    :exec create-stobj-table)
  :corr-fn stbl-corr
  :exports ((stbl-get :logic stbl-get$a :exec tbl-get :updater stbl-put) (stbl-put :logic stbl-put$a :exec tbl-put)
    (stbl-boundp :logic stbl-boundp$a :exec tbl-boundp)
    (stbl-rem :logic stbl-rem$a :exec tbl-rem)
    (stbl-count :logic stbl-count$a :exec tbl-count)
    (stbl-clear :logic stbl-clear$a :exec tbl-clear)
    (stbl-init :logic stbl-init$a :exec tbl-init)))