		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-scopeexprlist-mark-solo

Signature
(vl-scopeexprlist-mark-solo mtype x ss st ctx) → new-st
Arguments: mtype — Guard (member mtype '(:used :set)).; x — Guard (vl-scopeexprlist-p x).; ss — Guard (vl-scopestack-p ss).; st — Guard (vl-lucidstate-p st).; ctx — Guard (vl-lucidctx-p ctx).
Returns: new-st — Type (vl-lucidstate-p new-st).

Definitions and Theorems

Function: vl-scopeexprlist-mark-solo

(defun vl-scopeexprlist-mark-solo (mtype x ss st ctx)
  (declare (xargs :guard (and (member mtype '(:used :set))
                              (vl-scopeexprlist-p x)
                              (vl-scopestack-p ss)
                              (vl-lucidstate-p st)
                              (vl-lucidctx-p ctx))))
  (let ((__function__ 'vl-scopeexprlist-mark-solo))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (vl-lucidstate-fix st))
         (st (vl-hidsolo-mark mtype nil (car x)
                              ss st ctx)))
      (vl-scopeexprlist-mark-solo mtype (cdr x)
                                  ss st ctx))))

Theorem: vl-lucidstate-p-of-vl-scopeexprlist-mark-solo

(defthm vl-lucidstate-p-of-vl-scopeexprlist-mark-solo
  (b* ((new-st (vl-scopeexprlist-mark-solo mtype x ss st ctx)))
    (vl-lucidstate-p new-st))
  :rule-classes :rewrite)

Theorem: vl-scopeexprlist-mark-solo-of-vl-scopeexprlist-fix-x

(defthm vl-scopeexprlist-mark-solo-of-vl-scopeexprlist-fix-x
  (equal (vl-scopeexprlist-mark-solo mtype (vl-scopeexprlist-fix x)
                                     ss st ctx)
         (vl-scopeexprlist-mark-solo mtype x ss st ctx)))

Theorem: vl-scopeexprlist-mark-solo-vl-scopeexprlist-equiv-congruence-on-x

(defthm
  vl-scopeexprlist-mark-solo-vl-scopeexprlist-equiv-congruence-on-x
  (implies
       (vl-scopeexprlist-equiv x x-equiv)
       (equal (vl-scopeexprlist-mark-solo mtype x ss st ctx)
              (vl-scopeexprlist-mark-solo mtype x-equiv ss st ctx)))
  :rule-classes :congruence)

Theorem: vl-scopeexprlist-mark-solo-of-vl-scopestack-fix-ss

(defthm vl-scopeexprlist-mark-solo-of-vl-scopestack-fix-ss
  (equal (vl-scopeexprlist-mark-solo mtype x (vl-scopestack-fix ss)
                                     st ctx)
         (vl-scopeexprlist-mark-solo mtype x ss st ctx)))

Theorem: vl-scopeexprlist-mark-solo-vl-scopestack-equiv-congruence-on-ss

(defthm
    vl-scopeexprlist-mark-solo-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-scopeexprlist-mark-solo mtype x ss st ctx)
              (vl-scopeexprlist-mark-solo mtype x ss-equiv st ctx)))
  :rule-classes :congruence)

Theorem: vl-scopeexprlist-mark-solo-of-vl-lucidstate-fix-st

(defthm vl-scopeexprlist-mark-solo-of-vl-lucidstate-fix-st
  (equal
       (vl-scopeexprlist-mark-solo mtype x ss (vl-lucidstate-fix st)
                                   ctx)
       (vl-scopeexprlist-mark-solo mtype x ss st ctx)))

Theorem: vl-scopeexprlist-mark-solo-vl-lucidstate-equiv-congruence-on-st

(defthm
    vl-scopeexprlist-mark-solo-vl-lucidstate-equiv-congruence-on-st
  (implies
       (vl-lucidstate-equiv st st-equiv)
       (equal (vl-scopeexprlist-mark-solo mtype x ss st ctx)
              (vl-scopeexprlist-mark-solo mtype x ss st-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-scopeexprlist-mark-solo-of-vl-lucidctx-fix-ctx

(defthm vl-scopeexprlist-mark-solo-of-vl-lucidctx-fix-ctx
 (equal
    (vl-scopeexprlist-mark-solo mtype x ss st (vl-lucidctx-fix ctx))
    (vl-scopeexprlist-mark-solo mtype x ss st ctx)))

Theorem: vl-scopeexprlist-mark-solo-vl-lucidctx-equiv-congruence-on-ctx

(defthm
     vl-scopeexprlist-mark-solo-vl-lucidctx-equiv-congruence-on-ctx
  (implies
       (vl-lucidctx-equiv ctx ctx-equiv)
       (equal (vl-scopeexprlist-mark-solo mtype x ss st ctx)
              (vl-scopeexprlist-mark-solo mtype x ss st ctx-equiv)))
  :rule-classes :congruence)