		Search-engine friendly clone of the ACL2 documentation.

Defchoose-queries

Defchoose-bound-vars

Bound variables of a function introduced via defchoose.

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

The bound variables are in the third element of the defchoose event, which is either a single bound variable or a non-empty list of bound variables.

Definitions and Theorems

Function: defchoose-bound-vars

(defun defchoose-bound-vars (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defchoose-namep fn wrld))))
  (let ((__function__ 'defchoose-bound-vars))
    (declare (ignorable __function__))
    (let* ((event (get-event fn wrld))
           (bound-var/bound-vars (third event)))
      (if (symbolp bound-var/bound-vars)
          (list bound-var/bound-vars)
        bound-var/bound-vars))))