		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Dynamic-environments

Dynamic environments.

Leo code executes in the context of information including the values stored in the variables and constants that may be accessed, the functions that may be called, and so on. This information is captured by the notion of dynamic environment, which is formalized here.

Fixtype names for dynamic environments and their components include parts dinfo and denv, which stand for `dynamic information' and `dynamic environment'. Compare with static environments.

Subtopics

Call-dinfo: Fixtype of dynamic information about function calls.
Denv: Fixtype of dynamic environments.
Update-var/const-dinfo-in-scope-list: Update the dynamic information for a variable or constant in a list of scopes.
Update-var/const-dinfo-in-scope: Update the dynamic information for a variable or constant in a scope.
Var/const-dinfo: Fixtype of dynamic information about variables and constants.
Update-var/const-dinfo: Update the dynamic information for a variable or constant in a dynamic environment.
Add-var/const-dinfo-to-scope: Add dynamic information about a new variable or constant to a scope.
Add-var/const-dinfo: Add dynamic information about a new variable or constant to a dynamic environment.
Var/const-dinfo-option: Fixtype of optional dynamic information about variables and constants.
Get-var/const-dinfo-from-scope-list: Get the information about a variable or constant from a list of scopes.
Denv-option: Fixtype of optional dynamic environments.
Get-var/const-dinfo-from-scope: Get the information about a variable or constant from a scope.
Vcscope-dinfo-option: Fixtype of optional dynamic information about scopes of variables and constants.
Vcscope-dinfo-list-option: Fixtype of optional lists of dynamic information about lists of scopes of variables and constants.
Vcscope-dinfo: Fixtype of dynamic information about scopes of variables and constants.
Screens: Screens where console printing goes.
Get-var/const-dinfo: Get the information about a variable a constant from a dynamic environment.
Vcscope-dinfo-option-result: Fixtype of errors and optional dynamic information about scopes of variables and constants.
Vcscope-dinfo-list-result: Fixtype of errors and lists of dynamic information about scopes of variables and constants.
Vcscope-dinfo-result: Fixtype of errors and dynamic information about scopes of variables and constants.
Dynamic-struct-environments: Dynamic environments for struct types in Leo.
Dynamic-function-environments: Dynamic environments for functions in Leo.
Denv-result: Fixtype of errors and dynamic environments.
Init-denv: Initial dynamic environment.
Vcscope-dinfo-list: Fixtype of lists of dynamic information about scopes of variables and constants.
Call-dinfo-list: Fixtype of lists of dynamic information about function calls.