		Search-engine friendly clone of the ACL2 documentation.

Find-base-cases

Find-a-base-case

Signature
(find-a-base-case term fns fake-fns prefer-then state) → base-case
Arguments: fns — Guard (symbol-listp fns).; fake-fns — Guard (and (symbol-alistp fake-fns) (nat-listp (strip-cdrs fake-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 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

(defun find-a-base-case (term fns fake-fns prefer-then state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp fns)
                             (and (symbol-alistp fake-fns)
                                  (nat-listp (strip-cdrs fake-fns)))
                             (booleanp prefer-then))))
 (let ((__function__ 'find-a-base-case))
   (declare (ignorable __function__))
   (mv-let (erp all-base largest)
           (find-a-base-case-aux
                term (append fns (strip-cars fake-fns))
                prefer-then
                (acl2::add-fake-fns-to-world fake-fns (w state))
                state)
     (cond (erp (hard-error 'find-a-base-case
                            "Cannot find a base case!" nil))
           (all-base term)
           (t largest)))))