other
(in-package "ACL2")
table-programmaticfunction
(defun table-programmatic (table-name key-name value wrld) (declare (xargs :guard (and (symbolp table-name) (plist-worldp wrld)))) (let ((old-alist (table-alist table-name wrld))) (if (not (alistp old-alist)) (er hard? 'table-programmatic "Table-alist for ~x0 is not an alist: ~x1." table-name old-alist) (putprop table-name 'table-alist (put-assoc-equal key-name value old-alist) wrld))))
overwrite-table-programmaticfunction
(defun overwrite-table-programmatic (table-name alist state) (declare (xargs :mode :program :stobjs state)) (with-output! :off :all (table-fn table-name (list nil (kwote alist) :clear) state `(table ,TABLE-NAME nil ',ALIST :clear))))
set-table-entry-programmaticfunction
(defun set-table-entry-programmatic (table-name key value state) (declare (xargs :guard (symbolp table-name) :mode :program :stobjs state)) (with-output! :off :all (table-fn table-name (list (kwote key) (kwote value)) state `(table ,TABLE-NAME nil ',KEY ',VALUE))))