		Search-engine friendly clone of the ACL2 documentation.

String-utilities

Some utilities for strings (and characters).

These utilities may be eventually integrated into std/strings.

Code-char-injectivity-theorem: code-char is injective on natural numbers below 256.
8bitbytes-hexchars-conversions: Conversions from 8-bit bytes to lists of hex character digits.
Code-char-inverses-theorems: code-char and char-code are mutual inverses.
String-kinds: Predicates that characterize various kinds of strings.
String-codelist-conversions: Conversions between strings and lists of character codes.
Charlist-codelist-conversions: Conversions between lists of characters and lists of codes.
8bitbytes-hexstrings-conversions: Conversions from 8-bit bytes to strings of hex character digits.