		Search-engine friendly clone of the ACL2 documentation.

Svmods

Modhier-measure

Signature
(modhier-measure x modalist) → acl2::res
Returns: acl2::res — Type (o-p acl2::res).

Definitions and Theorems

Function: modhier-measure

(defun modhier-measure (x modalist)
  (declare (xargs :guard t))
  (let ((__function__ 'modhier-measure))
    (declare (ignorable __function__))
    (nat-list-measure
         (list (b* (((mv acl2::res acl2::memo)
                     (modhier-depth-memo x nil modalist)))
                 (fast-alist-free acl2::memo)
                 acl2::res)
               0 0))))

Theorem: o-p-of-modhier-measure

(defthm o-p-of-modhier-measure
  (b* ((acl2::res (modhier-measure x modalist)))
    (o-p acl2::res))
  :rule-classes :rewrite)