A collection of very basic functions that are occasionally convenient.

The

- 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 thatx is a natural number and, in the execution, it is just a no-op that returnsx .- 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" . - Std/basic-extensions
- Extensions of Std/basic in the Kestrel Books.
- 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.
- Symbol-package-name-lst
- Lift
`symbol-package-name`to lists. - 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.- 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`. - Lifix
`(lifix x)`is logically identical to(ifix x) , but its guard requires thatx is an integer and, in the execution, it is just a no-op that returnsx .- 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 justb . - 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/member-symbol-name
- Theorems about the built-in function
member-symbol-name . - False
- A function that just returns the constant
nil .