Value
Fixtype of values.
This is a tagged union type, introduced by fty::deftagsum.
Member Tags → Types
- :number → value-number
- :character → value-character
- :string → value-string
- :symbol → value-symbol
- :cons → value-cons
The ACL2 values of the evaluation semantics are
numbers, characters, strings, symbols, and cons pairs.
See the discussion in symbol-value for why
we do not use the built-in ACL2 symbols here.
The ACL2 logical semantics also allows
additional values called `bad atoms',
and consequently cons pairs
that may contain them directly or indirectly.
However, such values cannot be constructed in evaluation,
and therefore are not formalized here,
where we are only concerned with the ACL2 programming language,
not the ACL2 logic.
Note that the constructors
value-number,
value-character, and
value-string
lift ACL2 numbers, characters, and symbols to the meta level,
analogously to lift-symbol for symbols.
Note also that the accessors
value-number->get,
value-character->get, and
value-string->get
do the opposite, i.e. they lower numbers, characters, and strings
from the meta level,
analogously to lower-symbol.
On the other hand, the constructor value-cons
does not lift a cons pair to the meta level,
because it operates on two meta-level values.
See lift-value instead.
Subtopics
- Valuep
- Recognizer for value structures.
- Value-case
- Case macro for the different kinds of value structures.
- Value-fix
- Fixing function for value structures.
- Value-equiv
- Basic equivalence relation for value structures.
- Value-count
- Measure for recurring over value structures.
- Value-cons
- Value-symbol
- Value-string
- Value-number
- Value-character
- Value-kind
- Get the kind (tag) of a value structure.
