• 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
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
                • Atj-def-java-primitive-array-model
                • Short-array
                • Long-array
                • Int-array
                • Char-array
                • Byte-array
                • Boolean-array
                • Float-array
                  • Float-array-fix
                  • Float-array-equiv
                  • Make-float-array
                  • Float-array->components
                  • Change-float-array
                  • Float-arrayp
                  • Double-array
                  • Byte-array-to-sbyte8-list
                  • Short-array-to-sbyte16-list
                  • Long-array-to-sbyte64-list
                  • Int-array-to-sbyte32-list
                  • Char-array-to-ubyte16-list
                  • Boolean-array-to-boolean-list
                  • Double-array-write
                  • Boolean-array-write
                  • Short-array-write
                  • Short-array-from-sbyte16-list
                  • Long-array-write
                  • Int-array-write
                  • Float-array-write
                  • Char-array-write
                  • Char-array-from-ubyte16-list
                  • Byte-array-write
                  • Byte-array-from-sbyte8-list
                  • Boolean-array-from-boolean-list
                  • Long-array-from-sbyte64-list
                  • Int-array-from-sbyte32-list
                  • Short-array-new-init
                  • Double-array-index-in-range-p
                  • Byte-array-new-init
                  • Boolean-array-new-init
                  • Boolean-array-index-in-range-p
                  • Short-array-new-len
                  • Short-array-index-in-range-p
                  • Long-array-new-len
                  • Long-array-new-init
                  • Long-array-index-in-range-p
                  • Int-array-new-init
                  • Int-array-index-in-range-p
                  • Float-array-new-len
                  • Float-array-index-in-range-p
                  • Double-array-new-len
                  • Char-array-new-len
                  • Char-array-new-init
                  • Char-array-index-in-range-p
                  • Byte-array-new-len
                  • Byte-array-index-in-range-p
                  • Boolean-array-new-len
                  • Short-array-read
                  • Long-array-read
                  • Int-array-new-len
                  • Float-array-read
                  • Float-array-new-init
                  • Double-array-read
                  • Double-array-new-init
                  • Char-array-read
                  • Byte-array-read
                  • Boolean-array-read
                  • Int-array-read
                  • Short-array-length
                  • Float-array-length
                  • Double-array-length
                  • Boolean-array-length
                  • Long-array-length
                  • Int-array-length
                  • Char-array-length
                  • Byte-array-length
                • Atj-java-abstract-syntax
                • Atj-input-processing
                • Atj-java-pretty-printer
                • Atj-code-generation
                • Atj-java-primitives
                • Atj-java-primitive-arrays
                • Atj-type-macros
                • Atj-java-syntax-operations
                • Atj-fn
                • Atj-library-extensions
                • Atj-java-input-types
                • Atj-test-structures
                • Aij-notions
                • Atj-macro-definition
              • Atj-tutorial
            • Aij
            • Language
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Float-array

    Float-arrayp

    Recognizer for float-array structures.

    Signature
    (float-arrayp x) → *

    Definitions and Theorems

    Function: float-arrayp

    (defun float-arrayp (x)
      (declare (xargs :guard t))
      (let ((__function__ 'float-arrayp))
        (declare (ignorable __function__))
        (and (consp x)
             (eq (car x) :float-array)
             (true-listp (cdr x))
             (eql (len (cdr x)) 1)
             (b* ((components (std::da-nth 0 (cdr x))))
               (and (float-value-listp components)
                    (< (len components) (expt 2 31)))))))

    Theorem: consp-when-float-arrayp

    (defthm consp-when-float-arrayp
      (implies (float-arrayp x) (consp x))
      :rule-classes :compound-recognizer)