		Search-engine friendly clone of the ACL2 documentation.

Specific-types

Various specific fixtypes.

These complement the base types and the base list types.

Subtopics

Pos-list: Fixtype of lists of positive integers.
Defbyte-standard-instances: Standard fixtypes of unsigned and signed bytes of various sizes, with some accompanying theorems.
Defbytelist-standard-instances: Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.
Byte-list: A fixtype of true lists of (unsigned 8-bit) bytes.
Byte: A fixtype of (unsigned 8-bit) bytes.
Pos-option: Fixtype of optional positive integer numbers.
Nibble: A fixtype of (unsigned 4-bit) nibbles.
Nat-option: Fixtype of optional natural numbers.
String-option: Fixtype of optional strings.
Byte-list20: A fixtype of true lists of (unsigned 8-bit) bytes of length 20.
Byte-list32: A fixtype of true lists of (unsigned 8-bit) bytes of length 32.
Byte-list64: A fixtype of true lists of (unsigned 8-bit) bytes of length 64.
Pseudo-event-form: Fixtype of pseudo event forms.
Natoption/natoptionlist: Fixtype of optional natural numbers and lists of optional natural numbers.
Nati: A fixtype of natural numbers and infinity.
Character-list: Fixtype of lists of characters.
Nat/natlist: Fixtype of natural numbers and lists of natural numbers.
Maybe-string: Fixtype of optional strings.
Nibble-list: A fixtype of true lists of (unsigned 4-bit) nibbles.
Natoption/natoptionlist-result: Fixtype of errors and optional natural numbers and lists of optional natural numbers.
Nat/natlist-result: Fixtype of errors and natural numbers and lists or natural numbers.
Nat-option-list-result: Fixtype of errors and lists of optional natural numbers.
Set: A fixtype of osets.
String-result: Fixtype of errors and strings.
String-list-result: Fixtype of errors and lists of strings.
Nat-result: Fixtype of errors and natural numbers.
Nat-option-result: Fixtype of errors and optional natural numbers.
Nat-list-result: Fixtype of errors and lists of natural numbers.
Maybe-string-result: Fixtype of errors and optional strings.
Integer-result: Fixtype of errors and integers.
Character-result: Fixtype of errors and characters.
Character-list-result: Fixtype of errors and lists of characters.
Boolean-result: Fixtype of errors and booleans.
Map: A fixtype of omaps.
Bag: A fixtype of obags.
Pos-set: Fixtype of finite sets of positive integers.
Hex-digit-char-list: Fixtype of lists of hexadecimal digit characters.
Dec-digit-char-list: Fixtype of lists of decimal digit characters.
Nat-option-list: Fixtype of lists of optional natural numbers.
Symbol-set: Fixtype of finite sets of symbols.
String-set: Fixtype of finite sets of strings.
Pseudo-event-form-list: Fixtype of lists of pseudo event forms.
Nat-set: Fixtype of finite sets of natural numbers.
Oct-digit-char-list: Fixtype of lists of octal digit characters.
Bin-digit-char-list: Fixtype of lists of binary digit characters.
Bit-list: A fixtype of true lists of bits.