• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
            • Fmt
            • Msg
            • Cw
            • Set-evisc-tuple
            • Set-iprint
            • Print-control
            • Read-file-into-string
            • Std/io
              • Open-channel-lemmas
              • Std/io/read-char$
              • Std/io/read-object
              • Std/io/open-output-channel
              • Unsound-read
              • Read-string
              • Read-bytes$
                • Read-64ule
                • Read-64ube
                • Read-64sle
                • Read-64sbe
                • Read-32ule
                • Read-32sle
                • Read-32sbe
                • Read-32ube
                • Read-16sle
                • Read-16sbe
                • Read-16ule
                • Read-16ube
                • Read-8s
                • Combine-functions
                  • Combine64u
                  • Combine64s
                  • Combine32u
                  • Combine32s
                  • Combine16u
                  • Combine16s
              • File-measure
              • Read-bytes$-n
              • Std/io/read-byte$
              • Std/io/open-input-channel
              • Read-file-lines-no-newlines
              • Print-compressed
              • Nthcdr-bytes
              • Read-file-lines
              • Std/io/close-output-channel
              • Read-file-characters
              • Read-file-bytes
              • Print-legibly
              • Std/io/close-input-channel
              • Read-file-objects
              • Logical-story-of-io
              • Take-bytes
              • Std/io/peek-char$
              • Read-file-characters-rev
              • Read-file-as-string
              • Std/io/write-byte$
              • Std/io/set-serialize-character
              • Std/io/print-object$
              • Std/io/princ$
              • Std/io/read-file-into-string
              • *file-types*
            • Msgp
            • Printing-to-strings
            • Evisc-tuple
            • Output-controls
            • Observation
            • *standard-co*
            • Ppr-special-syms
            • Standard-oi
            • Standard-co
            • Without-evisc
            • Serialize
            • Output-to-file
            • Fmt-to-comment-window
            • Princ$
            • Character-encoding
            • Open-output-channel!
            • Cw-print-base-radix
            • Set-print-case
            • Set-print-base
            • Print-object$
            • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
            • Fmt1!
            • Fmt-to-comment-window!+
            • Read-file-into-byte-array-stobj
            • Fmt1
            • Fmt-to-comment-window+
            • Cw-print-base-radix!
            • Read-file-into-character-array-stobj
            • Fmx
            • Cw!+
            • Read-objects-from-book
            • Newline
            • Cw+
            • Probe-file
            • Write-objects-to-file!
            • Write-objects-to-file
            • Read-objects-from-file
            • Read-object-from-file
            • Read-file-into-byte-list
            • Set-fmt-soft-right-margin
            • Read-file-into-character-list
            • Io-utilities
          • Wormhole
          • Programming-with-state
          • W
          • Set-state-ok
          • Random$
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
            • Open-channel-lemmas
            • Std/io/read-char$
            • Std/io/read-object
            • Std/io/open-output-channel
            • Unsound-read
            • Read-string
            • Read-bytes$
              • Read-64ule
              • Read-64ube
              • Read-64sle
              • Read-64sbe
              • Read-32ule
              • Read-32sle
              • Read-32sbe
              • Read-32ube
              • Read-16sle
              • Read-16sbe
              • Read-16ule
              • Read-16ube
              • Read-8s
              • Combine-functions
                • Combine64u
                • Combine64s
                • Combine32u
                • Combine32s
                • Combine16u
                • Combine16s
            • File-measure
            • Read-bytes$-n
            • Std/io/read-byte$
            • Std/io/open-input-channel
            • Read-file-lines-no-newlines
            • Print-compressed
            • Nthcdr-bytes
            • Read-file-lines
            • Std/io/close-output-channel
            • Read-file-characters
            • Read-file-bytes
            • Print-legibly
            • Std/io/close-input-channel
            • Read-file-objects
            • Logical-story-of-io
            • Take-bytes
            • Std/io/peek-char$
            • Read-file-characters-rev
            • Read-file-as-string
            • Std/io/write-byte$
            • Std/io/set-serialize-character
            • Std/io/print-object$
            • Std/io/princ$
            • Std/io/read-file-into-string
            • *file-types*
          • Msgp
          • Printing-to-strings
          • Evisc-tuple
          • Output-controls
          • Observation
          • *standard-co*
          • Ppr-special-syms
          • Standard-oi
          • Standard-co
          • Without-evisc
          • Serialize
          • Output-to-file
          • Fmt-to-comment-window
          • Princ$
          • Character-encoding
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Extend-pathname
          • Print-object$+
          • Fmx-cw
          • Set-print-radix
          • Set-fmt-hard-right-margin
          • File-write-date$
          • Proofs-co
          • Set-print-base-radix
          • Print-base-p
          • *standard-oi*
          • Wof
          • File-length$
          • Fms!-lst
          • Delete-file$
          • *standard-ci*
          • Write-list
          • Trace-co
          • Fmt!
          • Fms
          • Cw!
          • Fmt-to-comment-window!
          • Fms!
          • Eviscerate-hide-terms
          • Fmt1!
          • Fmt-to-comment-window!+
          • Read-file-into-byte-array-stobj
          • Fmt1
          • Fmt-to-comment-window+
          • Cw-print-base-radix!
          • Read-file-into-character-array-stobj
          • Fmx
          • Cw!+
          • Read-objects-from-book
          • Newline
          • Cw+
          • Probe-file
          • Write-objects-to-file!
          • Write-objects-to-file
          • Read-objects-from-file
          • Read-object-from-file
          • Read-file-into-byte-list
          • Set-fmt-soft-right-margin
          • Read-file-into-character-list
          • Io-utilities
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
        • Packages
        • Oracle-eval
        • Defmacro-untouchable
        • <<
        • Primitive
        • Revert-world
        • Unmemoize
        • Set-duplicate-keys-action
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Fake-oracle-eval
        • Defopen
        • Sleep
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Read-bytes$

Combine-functions

Optimized byte-combining functions.

Subtopics

Combine64u
(combine64u a7 a6 a5 a4 a3 a2 a1 a0) merges unsigned bytes, producing the 64-bit unsigned interpretation of {a7, a6, a5, a4, a3, a2, a1, a0}.
Combine64s
(combine64s a7 a6 a5 a4 a3 a2 a1 a0) merges unsigned bytes, producing the 64-bit unsigned interpretation of {a7, a6, a5, a4, a3, a2, a1, a0}.
Combine32u
(combine32u a3 a2 a1 a0) merges unsigned bytes, producing the 32-bit unsigned interpretation of (a3 << 24) | (a2 << 16) | (a1 << 8) | a0.
Combine32s
(combine32s a3 a2 a1 a0) merges unsigned bytes, producing the 32-bit signed interpretation of (a3 << 24) | (a2 << 16) | (a1 << 8) | a0.
Combine16u
(combine16u a1 a0) merges unsigned bytes, producing the 16-bit unsigned interpretation of (a1 << 8) | a0.
Combine16s
(combine16s a1 a0) merges unsigned bytes, producing the 16-bit signed interpretation of (a1 << 8) | a0.