		Search-engine friendly clone of the ACL2 documentation.

Binary

Functions for working with binary numbers in strings.

Parse-bits-from-string: Parse a binary number from a string, at some offset.
Parse-bits-from-charlist: Parse a binary number from the beginning of a character list.
Nat-to-bin-chars: Convert a natural number into a list of bits.
Bin-digit-chars-value: Coerces a list of bit digits into a natural number.
Take-leading-bin-digit-chars: Collect any leading 0-1 characters from the start of a character list.
Bin-digit-char-listp: Recognize lists of binary digit characters.
Skip-leading-bit-digits: Skip over any leading 0-1 characters at the start of a character list.
Bin-digit-char-list*p: Recognizes lists of bin-digit-char-p characters.
Bin-digit-string-p: Recognizer for strings whose characters are all 0 or 1.
Bin-digit-char-value: Coerces a bin-digit-char-p character into a number, 0 or 1.
Strval2: Interpret a string as a binary number.
Nat-to-bin-string: Convert a natural number into a string with its bits.
Bin-digit-char-p: Recognizer for characters #\0 and #\1.
Nat-to-bin-string-list: Convert a list of natural numbers into a list of bit strings.
Nat-to-bin-string-size: Number of characters in the binary representation of a natural.
Revappend-nat-to-bin-chars: More efficient version of (revappend (nat-to-bin-chars n) acc).
Binify-width: Convert numbers into readable binary strings, fixing the number of digits printed
Binify: Convert numbers into readable binary strings.