		Search-engine friendly clone of the ACL2 documentation.

Defchoose-queries

Defchoose-body

Translated body of a function introduced via defchoose.

Signature
(defchoose-body fn wrld) → body
Arguments: fn — Guard (defchoose-namep fn wrld).; wrld — Guard (plist-worldp wrld).
Returns: body — A pseudo-termp.

The body body is extracted from the constraining axiom of fn, which has one of the following forms (see defchoose-constraint in the ACL2 source code):

(implies body ...), if :strengthen is nil and fn has one bound variable.
(if ... (implies body ...) nil), if strengthen is nil and fn has more than one bound variable.
(if (implies body ...) ... nil), if :strengthen is t and fn has one bound variable.
(if (if ... (implies body ...) nil) ... nil), if strengthen is t and fn has more than one bound variable.

Definitions and Theorems

Function: defchoose-body

(defun defchoose-body (fn wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (defchoose-namep fn wrld))))
  (let ((__function__ 'defchoose-body))
    (declare (ignorable __function__))
    (b* ((axiom (defchoosep fn wrld))
         (strengthen (defchoose-strengthen fn wrld))
         (bound-vars (defchoose-bound-vars fn wrld))
         (one-bound-var (= (len bound-vars) 1)))
      (if strengthen (if one-bound-var (second (second axiom))
                       (second (third (second axiom))))
        (if one-bound-var (second axiom)
          (second (third axiom)))))))