• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
        • Deftagsum
        • Defprod
        • Defflexsum
        • Defbitstruct
        • Deflist
        • Defalist
        • Defbyte
        • Deffixequiv
        • Defresult
        • Deffixtype
        • Defoption
        • Fty-discipline
        • Fold
        • Fty-extensions
          • Defbyte
          • Defresult
          • Fold
          • Defsubtype
          • Defset
          • Specific-types
          • Defflatsum
          • Deflist-of-len
          • Pos-list
          • Defbytelist
          • Defomap
          • Defbyte-standard-instances
          • Deffixtype-alias
          • Defbytelist-standard-instances
          • Defunit
          • Byte-list
          • Byte
          • Database
          • Pos-option
          • Nibble
          • Nat-option
          • String-option
          • Byte-list20
          • Byte-list32
          • Byte-list64
          • Pseudo-event-form
          • Natoption/natoptionlist
          • Nati
          • Character-list
          • Nat/natlist
          • Maybe-string
          • Nibble-list
          • Natoption/natoptionlist-result
          • Nat/natlist-result
          • Nat-option-list-result
          • Set
          • String-result
          • String-list-result
          • Nat-result
          • Nat-option-result
          • Nat-list-result
          • Maybe-string-result
          • Integer-result
          • Character-result
          • Character-list-result
          • Boolean-result
          • Map
          • Bag
          • Pos-set
          • Hex-digit-char-list
          • Dec-digit-char-list
          • Pseudo-event-form-list
          • Nat-option-list
          • Symbol-set
          • String-set
          • Nat-set
          • Oct-digit-char-list
          • Bin-digit-char-list
          • Bit-list
        • Defsubtype
        • Defset
        • Deftypes
        • Specific-types
        • Defflatsum
        • Deflist-of-len
        • Defbytelist
        • Fty::basetypes
        • Defomap
        • Defvisitors
        • Deffixtype-alias
        • Deffixequiv-sk
        • Defunit
        • Multicase
        • Deffixequiv-mutual
        • Fty::baselists
        • Def-enumcase
        • Defmap
      • Apt
      • Std/util
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • Soft
      • Defthm-domain
      • Event-macros
      • Def-universal-equiv
      • Def-saved-obligs
      • With-supporters-after
      • Definec
      • Sig
      • Outer-local
      • Data-structures
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Kestrel-books
  • Fty

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.