		Search-engine friendly clone of the ACL2 documentation.

Svex-rewrite-trace-profile

Svex-sneaky-prof-mutator

A ACL2::sneaky mutator for profiling.

Signature
(svex-sneaky-prof-mutator val name-localp) → *
Arguments: val — Guard (consp val).; name-localp — Guard (consp name-localp).

Definitions and Theorems

Function: svex-sneaky-prof-mutator

(defun svex-sneaky-prof-mutator (val name-localp)
  (declare (xargs :guard (and (consp val) (consp name-localp))))
  (let ((__function__ 'svex-sneaky-prof-mutator))
    (declare (ignorable __function__))
    (b* ((val (car val))
         ((mv nonloc loc)
          (if (consp val)
              (mv (car val) (cdr val))
            (mv nil nil))))
      (list (cons (car name-localp)
                  (if (cdr name-localp)
                      (cons nonloc (+ 1 (fix loc)))
                    (cons (+ 1 (fix nonloc)) loc)))))))