Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
100-theorems
Arithmetic
Bit-vectors
Sparseint
Bitops
Bitops/merge
Bitops-compatibility
Bitops-books
Logbitp-reasoning
Bitops/signed-byte-p
Fast-part-select
Bitops/integer-length
Bitops/extra-defs
Install-bit
Trailing-0-count
Bitops/defaults
Logbitp-mismatch
Trailing-1-count
Bitops/rotate
Rotate-right
Rotate-left
Rotate-right-1
Rotate-left-1
Rotate-right**
Rotate-left**
Bitops/equal-by-logbitp
Bitops/ash-bounds
Bitops/fast-logrev
Limited-shifts
Bitops/part-select
Bitops/parity
Bitops/saturate
Bitops/part-install
Bitops/logbitp-bounds
Bitops/ihsext-basics
Bitops/fast-rotate
Bitops/fast-logext
Bitops/ihs-extensions
Bv
Ihs
Rtl
Algebra
Testing-utilities
Bitops
Bitops/rotate
Definitions of
rotate-left
and
rotate-right
operations, and lemmas for reasoning about them.
Subtopics
Rotate-right
Rotate a bit-vector some arbitrary number of places to the right.
Rotate-left
Rotate a bit-vector some arbitrary number of places to the left.
Rotate-right-1
Rotate a bit-vector by a single place to the right.
Rotate-left-1
Rotate a bit-vector by a single place to the left.
Rotate-right**
Alternate, recursive definitions of
rotate-right
.
Rotate-left**
Alternate, recursive definitions of
rotate-left
.
