		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Values

Leo values.

These are the entities that are manipulated at run time. We formalize them as being tagged by their types (as common in programming language formalizations), which lets us express precisely the type correctness requirements in our defensive operational semantics.

Subtopics

Int-valuep: Recognizer of Leo integer values.
Value-option: Fixtype of optional Leo values.
Type-of-value: Leo type of a Leo value.
Value-option-result: Fixtype of optional Leo values and errors.
Value-list-result: Fixtype of lists of Leo values and errors.
Name+value: Fixtype of pairs consisting of a name (identifier) and a value.
Value-result: Fixtype of Leo values and errors.
Make-int-value: Makes an integer value or an error.
Type-map-of-value-map: Type map corresponding to a value map.
Name+type-of-name+value: Name-type pair corresponding to a name-value pair.
Int-value-bound-theorems: Theorems about the bounds of the integer values.
Int-value-to-int: ACL2 integer value corresponding to a Leo integer value.
Int-value-numbits: Returns the number of bits that a value of this kind could take.
Value/valuelist
*most-positive-i8*
*most-positive-i64*
*most-positive-i32*
*most-positive-i16*
*most-positive-i128*
*most-negative-i8*
*most-negative-i64*
*most-negative-i32*
*most-negative-i16*
*most-negative-i128*
*greatest-u8*
*greatest-u64*
*greatest-u32*
*greatest-u16*
*greatest-u128*