Function table for a list of function definitions.
(funtable-for-fundefs fundefs) → funtab
We go through the list and form a function table for the functions. It is an error if there are two functions with the same name.
Function:
(defun funtable-for-fundefs (fundefs) (declare (xargs :guard (fundef-listp fundefs))) (let ((__function__ 'funtable-for-fundefs)) (declare (ignorable __function__)) (b* (((when (endp fundefs)) nil) ((okf funtab) (funtable-for-fundefs (cdr fundefs))) (fundef (car fundefs)) (fun (fundef->name fundef)) ((when (consp (omap::assoc fun funtab))) (reserrf (list :duplicate-function fun)))) (omap::update fun (funtype-for-fundef fundef) funtab))))
Theorem:
(defthm funtable-resultp-of-funtable-for-fundefs (b* ((funtab (funtable-for-fundefs fundefs))) (funtable-resultp funtab)) :rule-classes :rewrite)
Theorem:
(defthm funtable-for-fundefs-of-fundef-list-fix-fundefs (equal (funtable-for-fundefs (fundef-list-fix fundefs)) (funtable-for-fundefs fundefs)))
Theorem:
(defthm funtable-for-fundefs-fundef-list-equiv-congruence-on-fundefs (implies (fundef-list-equiv fundefs fundefs-equiv) (equal (funtable-for-fundefs fundefs) (funtable-for-fundefs fundefs-equiv))) :rule-classes :congruence)