		Search-engine friendly clone of the ACL2 documentation.

Fty-extensions

Extensions of FTY in the Kestrel Books.

These could be merged with FTY at some point.

Subtopics

Defbyte: Introduce a fixtype of unsigned or signed bytes of a specified size.
Defresult: Introduce a fixtype for good results and error results.
Fold: Notion of general folds for fixtypes.
Defsubtype: Introduce a fixtype that is a subtype of the given fixtype.
Defset: Generate a fixtype of osets whose elements have a specified fixtype.
Specific-types: Various specific fixtypes.
Defflatsum: Introduce a fixtype for the flat (i.e. not tagged) sum of disjoint fixtypes.
Deflist-of-len: Introduce a fixtype of lists of a specified length.
Pos-list: Fixtype of lists of positive integers.
Defbytelist: Introduce a fixtype of true lists of unsigned or signed bytes of a specified size.
Defomap: Generate a fixtype of omaps whose keys and values have specified fixtypes.
Defbyte-standard-instances: Standard fixtypes of unsigned and signed bytes of various sizes, with some accompanying theorems.
Deffixtype-alias: Introduce an alias of an existing fixtype.
Defbytelist-standard-instances: Standard fixtypes of true lists of unsigned and signed bytes of various sizes, with some accompanying theorems.
Defunit: Generate a singleton fixtype.
Byte-list: A fixtype of true lists of (unsigned 8-bit) bytes.
Byte: A fixtype of (unsigned 8-bit) bytes.
Database: Extensions for the FTY database.
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.
Pseudo-event-form-list: Fixtype of lists of pseudo event forms.
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.
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.