		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-dissect

Signature
(vl-lucid-dissect st) → reportcard
Arguments: st — Guard (vl-lucidstate-p st).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lucid-dissect

(defun vl-lucid-dissect (st)
  (declare (xargs :guard (vl-lucidstate-p st)))
  (let ((__function__ 'vl-lucid-dissect))
    (declare (ignorable __function__))
    (b* (((vl-lucidstate st))
         (copy (fast-alist-fork st.db nil))
         (- (fast-alist-free copy)))
      (vl-lucid-dissect-database copy nil st))))

Theorem: vl-reportcard-p-of-vl-lucid-dissect

(defthm vl-reportcard-p-of-vl-lucid-dissect
  (b* ((reportcard (vl-lucid-dissect st)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-lucid-dissect-of-vl-lucidstate-fix-st

(defthm vl-lucid-dissect-of-vl-lucidstate-fix-st
  (equal (vl-lucid-dissect (vl-lucidstate-fix st))
         (vl-lucid-dissect st)))

Theorem: vl-lucid-dissect-vl-lucidstate-equiv-congruence-on-st

(defthm vl-lucid-dissect-vl-lucidstate-equiv-congruence-on-st
  (implies (vl-lucidstate-equiv st st-equiv)
           (equal (vl-lucid-dissect st)
                  (vl-lucid-dissect st-equiv)))
  :rule-classes :congruence)