		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-witness

Retrieve the name of the witness of a function introduced via defun-sk.

Signature
(defun-sk-witness fn wrld) → witness
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: witness — A symbolp.

For a function introduced via defun-sk, the name of the witness is the old constraint-lst property, now found in the constraint-lst-etc property. Retrieving it from there is faster than calculating it from fn and the options of the defun-sk.

Definitions and Theorems

Function: defun-sk-witness

(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__))
    (pre-v8-7-getpropc-constraint-lst-nil fn wrld)))