		Search-engine friendly clone of the ACL2 documentation.

Defun-sk-queries

Defun-sk-body

Retrieve the body of a function introduced via defun-sk.

Signature
(defun-sk-body fn wrld) → body
Arguments: fn — Guard (defun-sk-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: body — A pseudo-event-formp.

This is the sub-form (forall ...) or (exists ...) of the defun-sk form. Thus, the terms in this sub-from are untranslated.

In the defun-sk form, the body sub-form is obtained by first removing the keyed options (if any) and then taking the last element of the resulting list.

To retrieve the quantifier, bound variable, and matrix of this body, use defun-sk-quantifier, defun-sk-bound-vars, defun-sk-matrix, and defun-sk-imatrix.

Definitions and Theorems

Function: defun-sk-body

(defun defun-sk-body (fn wrld)
 (declare (xargs :guard (and (plist-worldp wrld)
                             (defun-sk-namep fn wrld))))
 (let ((__function__ 'defun-sk-body))
  (declare (ignorable __function__))
  (b*
   ((form (defun-sk-p fn wrld))
    ((mv erp form-without-keyed-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)))
   (car (last form-without-keyed-options)))))