		Search-engine friendly clone of the ACL2 documentation.

Variable-visibility-preservation

Var-visible-preservep-of-create-var

Preservation of variable visibility under create-var.

The predicate var-visible-preservep holds between a computation state and the one obtained from it via create-var.

This theorem is used, in var-visible-preservep-of-exec, to handle the execution of object declarations.

Definitions and Theorems

Theorem: var-visible-preservep-of-create-var

(defthm var-visible-preservep-of-create-var
  (b* ((compst1 (create-var var val compst)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (not (errorp compst1))
                  (identp var))
             (var-visible-preservep compst compst1))))