		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Var/const-dinfo

Fixtype of dynamic information about variables and constants.

This is a product type introduced by fty::defprod.

Fields

value — value
constp — booleanp

This captures the information associated to a variable or constant name in a dynamic environment. The information consists of the value stored in the variable or constant, and a flag indicating whether it is a variable or a constant.

Note that Leo has no undefined or null value: when a variable comes into existence, it immediately has a value. Thus, it is appropriate for this variable information to always have a value.

This fixtype is the dynamic counterpart of var/const-sinfo.

Subtopics

Var/const-dinfo-fix: Fixing function for var/const-dinfo structures.
Var/const-dinfo-equiv: Basic equivalence relation for var/const-dinfo structures.
Make-var/const-dinfo: Basic constructor macro for var/const-dinfo structures.
Var/const-dinfo->value: Get the value field from a var/const-dinfo.
Var/const-dinfo->constp: Get the constp field from a var/const-dinfo.
Change-var/const-dinfo: Modifying constructor for var/const-dinfo structures.
Var/const-dinfop: Recognizer for var/const-dinfo structures.