|
|
|---|
|
|
|
|---|
Formula of a named theorem.
(thm-formula thm wrld) → formula
This is a specialization of formula to named theorems, for which the second argument of formula is immaterial. Since formula is in program mode only because of the code that handles the cases in which the first argument is not the name of a theorem, we avoid calling formula and instead replicate the code that handles the case in which the first argument is the name of a theorem; thus, this utility is in logic mode and guard-verified.
See thm-formula+ for an enhanced variant of this utility.
Function:
(defun thm-formula (thm wrld) (declare (xargs :guard (and (symbolp thm) (plist-worldp wrld)))) (let ((__function__ 'thm-formula)) (declare (ignorable __function__)) (getpropc thm 'theorem nil wrld)))