|
|
|---|
|
|
|
|---|
Fixtype of Imp environments.
While it may be mathematically more convenient to define environments as total functions over all variables, in ACL2's first-order logic we need to use finite functions, which are captured by omaps. We use an omap from strings (i.e. variable names) to integers (i.e. variable values).
In effect, our semantics will regard all variables to be defined, with a default value even if they are not explicitly in the finite map.