Retrieve the name of the witness of
a function introduced via defun-sk.
(defun-sk-witness fn wrld) → witness
- fn — Guard (defun-sk-namep fn wrld).
- wrld — Guard (plist-worldp wrld).
- witness — A symbolp.
For a function introduced via defun-sk,
the name of the witness is the constraint-lst property.
Retrieving it from there is faster than
calculating it from fn and the options of the defun-sk.
Definitions and Theorems
(defun defun-sk-witness (fn wrld)
(declare (xargs :guard (and (plist-worldp wrld)
(defun-sk-namep fn wrld))))
(let ((__function__ 'defun-sk-witness))
(declare (ignorable __function__))
(getpropc fn 'constraint-lst nil wrld)))