		Search-engine friendly clone of the ACL2 documentation.

Fun-table-init

Create an initial function table.

This is just the empty map.

Function: fun-table-init

(defun fun-table-init nil
  (declare (xargs :guard t))
  (let ((__function__ 'fun-table-init))
    (declare (ignorable __function__))
    nil))

Theorem: fun-tablep-of-fun-table-init

(defthm fun-tablep-of-fun-table-init
  (b* ((funtab (fun-table-init)))
    (fun-tablep funtab))
  :rule-classes :rewrite)