Retrieve the body of a function introduced via defun-sk.
(defun-sk-body fn wrld) → body
This is the sub-form
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.
(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)))))