		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-bound-vars

Retrieve the bound variables of a function introduced via defun-sk.

Signature
(defun-sk-bound-vars fn wrld) → bound-vars
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: bound-vars — A symbol-listp.

Definitions and Theorems

Function: defun-sk-bound-vars

(defun defun-sk-bound-vars (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defun-sk-namep fn wrld))))
  (let ((__function__ 'defun-sk-bound-vars))
    (declare (ignorable __function__))
    (b* ((body (defun-sk-body fn wrld))
         (var/vars (second body)))
      (if (atom var/vars)
          (list var/vars)
        var/vars))))