Std/basic
A collection of very basic functions that are occasionally
convenient.
The std/basic library adds a number of very basic definitions
that are not built into ACL2. There's very little to this, it's generally just
a meant to be a home for very simple definitions that don't fit into bigger
libraries.
Subtopics
- Maybe-stringp
- Recognizer for strings and nil.
- Maybe-natp
- Recognizer for naturals and nil.
- Two-nats-measure
- An ordinal measure for admitting functions: lexicographic ordering of
two natural numbers.
- Impossible
- Prove that some case is unreachable using guards.
- Bytep
- Recognize unsigned 8-bit bytes.
- Nat-list-measure
- An ordinal measure for admitting functions: lexicographic ordering of
a list of natural numbers.
- Maybe-posp
- Recognizer for positive naturals and nil.
- Nibblep
- Recognize unsigned 4-bit bytes.
- Organize-symbols-by-pkg
- Organize a list of symbols by their packages.
- Organize-symbols-by-name
- Organize a list of symbols by their names.
- Lnfix
- (lnfix x) is logically identical to (nfix x), but its guard
requires that x is a natural number and, in the execution, it is just a
no-op that returns x.
- Good-valuep
- Check if a value is ``good''.
- Streqv
- Case-sensitive string equivalence test.
- Chareqv
- Case-sensitive character equivalence test.
- Symbol-package-name-non-cl
- The symbol-package-name of a symbol,
but not "COMMON-LISP".
- Arith-equivs
- Definitions for congruence reasoning about integers/naturals/bits.
- Induction-schemes
- A variety of basic, widely applicable induction schemes.
- Maybe-integerp
- Recognizer for integers and nil.
- Char-fix
- Coerce to a character.
- Pos-fix
- (pos-fix x) is a fixing function for posp: it is the
identity for positive integers, or returns 1 for any other object.
- Symbol-package-name-lst
- Lift symbol-package-name to lists.
- Mbt$
- Variant of mbt that allows any non-nil value.
- Maybe-bitp
- Recognizer for bits and nil.
- Good-pseudo-termp
- Check if a pseudo-term only contains good values,
i.e. no bad atoms.
- Str-fix
- Coerce to a string.
- Maybe-string-fix
- Fixer for maybe-stringp.
- Nonkeyword-listp
- Recognize lists of non-keywords.
- Lifix
- (lifix x) is logically identical to (ifix x), but its guard
requires that x is an integer and, in the execution, it is just a no-op
that returns x.
- Bfix
- Bit fix. (bfix b) is a fixing function for bitps. It
coerces any object to a bit (0 or 1) by coercing non-1 objects to 0.
- Std/basic/if*
- Rules about if*.
- Impliez
- Logical implication defined via if.
- Tuplep
- Recognizers for true-lists of some particular length.
- Std/basic/intern-in-package-of-symbol
- Lemmas about intern-in-package-of-symbol available in the
std/basic library.
- Lbfix
- Logical bit fix. (lbfix b) is logically identical to (bfix
b) but executes as the identity. It requires (bitp b) as a guard, and
expands to just b.
- Std/basic/symbol-name-lst
- Theorems about symbol-name-lst
in the Std/basic library.
- True
- A function that always just returns the constant t.
- Std/basic/rfix
- Rules about rfix.
- Std/basic/realfix
- Rules about realfix.
- Std/basic/member-symbol-name
- Theorems about the built-in function member-symbol-name.
- Std/basic/fix
- Rules about fix.
- False
- A function that just returns the constant nil.
- Std/basic/nfix
- Rules about nfix.
- Std/basic/ifix
- Rules about ifix.
