		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Parteval-case-of-old

Classify old into one of the three cases described in the reference documentation.

Signature
(parteval-case-of-old old$ static$ wrld) → case
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; wrld — Guard (plist-worldp wrld).
Returns: case — 1, 2, or 3.

Definitions and Theorems

Function: parteval-case-of-old

(defun parteval-case-of-old (old$ static$ wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbol-alistp static$)
                             (plist-worldp wrld))))
 (let ((__function__ 'parteval-case-of-old))
  (declare (ignorable __function__))
  (b*
   (((when (not (irecursivep old$ wrld))) 1)
    ((when (member-eq old$
                      (all-ffn-symbs (termination-theorem old$ wrld)
                                     nil)))
     3)
    ((when (parteval-unchanging-static-in-rec-calls-p
                (recursive-calls old$ wrld)
                old$ (strip-cars static$)
                wrld))
     2))
   3)))