		Search-engine friendly clone of the ACL2 documentation.

Interp-st-fn-annotation

Finds the annotation, if any, of the innermost nesting of fn on the stack.

Signature
(interp-st-fn-annotation fn interp-st) → annotation
Arguments: fn — Guard (pseudo-fnsym-p fn).
Returns: annotation — Type (fgl-object-p annotation).

Definitions and Theorems

Function: interp-st-fn-annotation

(defun interp-st-fn-annotation (fn interp-st)
  (declare (xargs :stobjs (interp-st)))
  (declare (xargs :guard (pseudo-fnsym-p fn)))
  (let ((__function__ 'interp-st-fn-annotation))
    (declare (ignorable __function__))
    (b* ((idx (interp-st-scan-for-fnsym 0 fn interp-st))
         ((unless idx) nil)
         ((when (<= (- (interp-st-full-scratch-len interp-st)
                       2)
                    idx))
          nil))
      (and (eq (interp-st-nth-scratch-kind (+ 2 idx)
                                           interp-st)
               :fnsym)
           (eq (interp-st-nth-scratch-fnsym (+ 2 idx)
                                            interp-st)
               'annotate)
           (eq (interp-st-nth-scratch-kind (+ 1 idx)
                                           interp-st)
               :fgl-obj)
           (interp-st-nth-scratch-fgl-obj (+ 1 idx)
                                          interp-st)))))

Theorem: fgl-object-p-of-interp-st-fn-annotation

(defthm fgl-object-p-of-interp-st-fn-annotation
  (b* ((annotation (interp-st-fn-annotation fn interp-st)))
    (fgl-object-p annotation))
  :rule-classes :rewrite)