|
|
|---|
|
|
|
|---|
Pretty-printer for debugging the lucid state.
(vl-pps-lucidstate x) → str
Function:
(defun vl-pps-lucidstate (x) (declare (xargs :guard (vl-lucidstate-p x))) (let ((__function__ 'vl-pps-lucidstate)) (declare (ignorable __function__)) (with-local-ps (vl-pp-lucidstate x))))
Theorem:
(defthm stringp-of-vl-pps-lucidstate (b* ((str (vl-pps-lucidstate x))) (stringp str)) :rule-classes :type-prescription)
Theorem:
(defthm vl-pps-lucidstate-of-vl-lucidstate-fix-x (equal (vl-pps-lucidstate (vl-lucidstate-fix x)) (vl-pps-lucidstate x)))
Theorem:
(defthm vl-pps-lucidstate-vl-lucidstate-equiv-congruence-on-x (implies (vl-lucidstate-equiv x x-equiv) (equal (vl-pps-lucidstate x) (vl-pps-lucidstate x-equiv))) :rule-classes :congruence)