Generate the name of the theorem saying that looking up a certain C function in the function environment yields the information for that function.
(atc-gen-cfun-fun-env-thm-name fn names-to-avoid wrld) → (mv name updated-names-to-avoid)
The actual theorem is generated in atc-gen-cfun-fun-env-thm. We separate out the generation of the theorem name because we need to use it in events that are computed before the actual theorem can be computed (see atc-gen-fundef).
Function:
(defun atc-gen-cfun-fun-env-thm-name (fn names-to-avoid wrld) (declare (xargs :guard (and (symbolp fn) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'atc-gen-cfun-fun-env-thm-name)) (declare (ignorable __function__)) (fresh-logical-name-with-$s-suffix (add-suffix-to-fn fn "-FUN-ENV") nil names-to-avoid wrld)))
Theorem:
(defthm symbolp-of-atc-gen-cfun-fun-env-thm-name.name (b* (((mv ?name ?updated-names-to-avoid) (atc-gen-cfun-fun-env-thm-name fn names-to-avoid wrld))) (symbolp name)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-cfun-fun-env-thm-name.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?name ?updated-names-to-avoid) (atc-gen-cfun-fun-env-thm-name fn names-to-avoid wrld))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)