		Search-engine friendly clone of the ACL2 documentation.

Find-base-cases

Find-a-base-case-translated

Find a base-case within a translated term.

Signature
(find-a-base-case-translated term fns prefer-then) → base-case
Arguments: term — Guard (pseudo-termp term).; fns — Guard (symbol-listp fns).; prefer-then — Guard (booleanp prefer-then).
Returns: base-case — Either a pseudo-termp representing the base-case, or a hard error. A hard error should not occur if term is the translated body of a valid function, and fns includes only symbols corresponding to the function or functions defined in mutual recursion with the function.

Definitions and Theorems

Function: find-a-base-case-translated

(defun find-a-base-case-translated (term fns prefer-then)
  (declare (xargs :guard (and (pseudo-termp term)
                              (symbol-listp fns)
                              (booleanp prefer-then))))
  (let ((__function__ 'find-a-base-case-translated))
    (declare (ignorable __function__))
    (mv-let (erp all-base largest)
            (find-a-base-case-translated-aux term fns prefer-then)
      (cond (erp (hard-error 'find-a-base-case-translated
                             "Cannot find a base case!" nil))
            (all-base term)
            (t largest)))))