• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
        • Representation
          • Representation-of-integer-operations
          • Atc-arrays
          • Representation-of-integers
            • Def-integer-values
            • Ushort-list-from-integer-list
            • Ullong-list-from-integer-list
            • Sshort-list-from-integer-list
            • Sllong-list-from-integer-list
            • Integer-list-from-ushort-list
            • Integer-list-from-ullong-list
            • Integer-list-from-sshort-list
            • Integer-list-from-sllong-list
            • Ulong-list-from-integer-list
            • Uchar-list-from-integer-list
            • Slong-list-from-integer-list
            • Schar-list-from-integer-list
            • Integer-list-from-ulong-list
            • Integer-list-from-uchar-list
            • Integer-list-from-slong-list
            • Integer-list-from-schar-list
            • Uint-list-from-integer-list
            • Sint-list-from-integer-list
            • Integer-list-from-uint-list
            • Integer-list-from-sint-list
            • Cinteger
            • Ullongp
            • Ucharp
            • Sintp
            • Ushortp
            • Ulongp
            • Uintp
            • Sllongp
            • Slongp
            • Sshortp
            • Scharp
            • Integer-from-sshort
            • Integer-from-sllong
            • Integer-from-sint
            • Integer-from-slong
            • Integer-from-schar
            • Integer-type-to-fixtype
            • Integer-from-ushort
            • Integer-from-ullong
            • Integer-from-uchar
            • Integer-from-cinteger
            • Integer-from-ulong
            • Integer-from-uint
            • Def-integer-values-loop
            • Sint-from-integer
            • Sint
            • Fixtype-to-integer-type
            • Uchar-from-integer
            • Ushort-from-integer-mod
            • Ushort-from-integer
            • Ulong-from-integer-mod
            • Ulong-from-integer
            • Ullong-from-integer-mod
            • Ullong-from-integer
            • Uchar-from-integer-mod
            • Sshort-from-integer
            • Slong-from-integer
            • Sllong-from-integer
            • Schar-from-integer
            • Uint-from-integer-mod
            • Uint-from-integer
            • Uchar
            • Schar
            • Ushort
            • Ulong
            • Ullong
            • Sshort
            • Slong
            • Sllong
            • Ullong-fix
            • Uint
            • Uchar-fix
            • Sint-fix
            • Ushort-fix
            • Ulong-fix
            • Uint-fix
            • Sshort-fix
            • Slong-fix
            • Sllong-fix
            • Schar-fix
            • Ushort-list
            • Ulong-list
              • Ulong-list-fix
              • Ulong-list-equiv
              • Ulong-listp
            • Ullong-list
            • Uint-list
            • Uchar-list
            • Sshort-list
            • Slong-list
            • Sllong-list
            • Sint-list
            • Schar-list
            • Integer-type-to/from-fixtype-theorems
            • *nonchar-integer-fixtypes*
          • Representation-of-integer-conversions
          • Pointed-integers
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Representation-of-integers

Ulong-list

Fixtype of lists of values of type unsigned long.

This is an ordinary fty::deflist.

Subtopics

Ulong-list-fix

(ulong-list-fix x) is a usual ACL2::fty list fixing function.

Ulong-list-equiv

Basic equivalence relation for ulong-list structures.

Ulong-listp

(ulong-listp x) recognizes lists where every element satisfies ulongp.