Modhier-list-measure-aux
- Signature
(modhier-list-measure-aux x acl2::memo modalist) → (mv * *)
Definitions and Theorems
Function: modhier-list-measure-aux
(defun modhier-list-measure-aux (x acl2::memo modalist)
(declare (xargs :guard t))
(let ((__function__ 'modhier-list-measure-aux))
(declare (ignorable __function__))
(if (atom x)
(mv 0 acl2::memo)
(b* (((mv acl2::res1 acl2::memo)
(modhier-depth-memo (car x)
acl2::memo modalist))
((mv acl2::res2 acl2::memo)
(modhier-list-measure-aux (cdr x)
acl2::memo modalist)))
(mv (max (if (eq acl2::res1 :loop) 0 acl2::res1)
acl2::res2)
acl2::memo)))))
