		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Fun-table-all-definedp

Check if all the functions in a table are defined.

Signature
(fun-table-all-definedp funtab) → yes/no
Arguments: funtab — Guard (fun-tablep funtab).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: fun-table-all-definedp

(defun fun-table-all-definedp (funtab)
  (declare (xargs :guard (fun-tablep funtab)))
  (let ((__function__ 'fun-table-all-definedp))
    (declare (ignorable __function__))
    (b* ((funtab (fun-table-fix funtab))
         ((when (omap::emptyp funtab)) t)
         ((mv & info) (omap::head funtab))
         ((unless (fun-sinfo->definedp info))
          nil))
      (fun-table-all-definedp (omap::tail funtab)))))

Theorem: booleanp-of-fun-table-all-definedp

(defthm booleanp-of-fun-table-all-definedp
  (b* ((yes/no (fun-table-all-definedp funtab)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: fun-table-all-definedp-of-fun-table-fix-funtab

(defthm fun-table-all-definedp-of-fun-table-fix-funtab
  (equal (fun-table-all-definedp (fun-table-fix funtab))
         (fun-table-all-definedp funtab)))

Theorem: fun-table-all-definedp-fun-table-equiv-congruence-on-funtab

(defthm fun-table-all-definedp-fun-table-equiv-congruence-on-funtab
  (implies (fun-table-equiv funtab funtab-equiv)
           (equal (fun-table-all-definedp funtab)
                  (fun-table-all-definedp funtab-equiv)))
  :rule-classes :congruence)