		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)