		Search-engine friendly clone of the ACL2 documentation.

Defchoose-queries

Defchoose-untrans-body

Untranslated body of a function introduced via defchoose.

Signature
(defchoose-untrans-body fn wrld) → *
Arguments: fn — Guard (defchoose-namep fn wrld).; wrld — Guard (plist-worldp wrld).

The untranslated body, as supplied by the user, is the fifth element of the defchoose event.

Definitions and Theorems

Function: defchoose-untrans-body

(defun defchoose-untrans-body (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defchoose-namep fn wrld))))
  (let ((__function__ 'defchoose-untrans-body))
    (declare (ignorable __function__))
    (fifth (get-event fn wrld))))