		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-options

Retrieve the keyed options of a function introduced via defun-sk.

Signature
(defun-sk-options fn wrld) → options
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: options — An alistp.

Definitions and Theorems

Function: defun-sk-options

(defun defun-sk-options (fn wrld)
 (declare (xargs :guard (and (plist-worldp wrld)
                             (defun-sk-namep fn wrld))))
 (let ((__function__ 'defun-sk-options))
  (declare (ignorable __function__))
  (b*
   ((form (defun-sk-p fn wrld))
    ((mv erp & options)
     (partition-rest-and-keyword-args form *defun-sk-keywords*))
    ((when erp)
     (raise
      "Internal error: ~
                           the DEFUN-SK form ~x0 of ~x1 is malformed."
      form fn)))
   options)))