(lookup-previous-stack-frame-binding var interp-st) → binding
Function:
(defun lookup-previous-stack-frame-binding (var interp-st) (declare (xargs :stobjs (interp-st))) (declare (xargs :guard (symbolp var))) (let ((__function__ 'lookup-previous-stack-frame-binding)) (declare (ignorable __function__)) (stobj-let ((stack (interp-st->stack interp-st))) (binding) (b* ((nframes (stack-frames stack)) ((when (< nframes 2)) nil) (minor (stack-nth-frame-minor-bindings 1 0 stack)) (minor-look (assoc-eq var minor)) ((when minor-look) (cdr minor-look)) (major (stack-nth-frame-bindings 1 stack))) (cdr (assoc-eq var major))) binding)))
Theorem:
(defthm fgl-object-p-of-lookup-previous-stack-frame-binding (b* ((binding (lookup-previous-stack-frame-binding var interp-st))) (fgl-object-p binding)) :rule-classes :rewrite)