		Search-engine friendly clone of the ACL2 documentation.

Transformation-tools

Variables-in-computation-states

Notions and theorems about variables in the computation states.

Transformations may need facts about certain variables being in the computation state and having values of certain types. Here we introduce a predicate to state that fact, along with some theorems about how execution relates to that predicate.

Subtopics

C::compustate-has-var-with-type-p: Check if a computation state includes a variable with a given name containing a value of the given type.
Exec-compustate-vars-theorems: Theorems about variables in computation states w.r.t. execution.
C::compustate-has-vars-with-types-p: Lift c::compustate-has-var-with-type-p to maps from identifiers to types, pointwise.
C::compustate-has-var-with-type-p-of-exit-exec-enter: Preservation of c::compustate-has-var-with-type-p after entering a new scope, executing a statement, and exiting the scope.
C::compustate-has-vars-with-types-p-of-exit-exec-enter: Preservation of c::compustate-has-vars-with-types-p after entering a new scope, executing a statement, and exiting the scope.
C::compustate-has-vars-with-types-p-of-enter-scope: Preservation of c::compustate-has-vars-with-types-p under c::enter-scope.
C::compustate-has-var-with-type-p-of-enter-scope: Preservation of c::compustate-has-var-with-type-p under c::enter-scope.