		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-p

Check if a named function has been introduced via defun-sk, returning the function's defun-sk form if the check succeeds.

Signature
(defun-sk-p fn wrld) → defun-sk-form?
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: defun-sk-form? — A maybe-pseudo-event-formp.

If the check fails, nil is returned.

As explained here, we consult the pe-table. If the defun-sk is generated by some other macros that also extends the table, the defun-sk form is not the only one associated to fn in the table. But it should be always the last one in the table entry for fn (which is an alist from absolute event numbers to forms), because none of the forms generated by defun-sk extends the table, and newer forms (generated by the hypothesized other macro that generates the defun-sk) are consed onto the entry.

This utility causes an error if called on a symbol that is not a function symbol.

Definitions and Theorems

Function: defun-sk-p

(defun defun-sk-p (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'defun-sk-p))
    (declare (ignorable __function__))
    (b* (((unless (function-symbolp fn wrld))
          (raise "The symbol ~x0 does not name a function."
                 fn))
         (table (table-alist 'pe-table wrld))
         (entry (cdr (assoc-eq fn table)))
         (last-number+form (car (last entry)))
         (last-form (cdr last-number+form)))
      (if (eq (car last-form) 'defun-sk)
          last-form
        nil))))