		Search-engine friendly clone of the ACL2 documentation.

Svmods

Modhier-loopfree-p

Signature
(modhier-loopfree-p x modalist) → *

Definitions and Theorems

Function: modhier-loopfree-p

(defun modhier-loopfree-p (x modalist)
  (declare (xargs :guard (and (modalist-p modalist) t)))
  (let ((__function__ 'modhier-loopfree-p))
    (declare (ignorable __function__))
    (b* (((mv acl2::res acl2::memo)
          (modhier-depth-memo x nil modalist)))
      (fast-alist-free acl2::memo)
      (not (eq acl2::res :loop)))))