Included Books
arith-equivs
bytep
defs
fix
good-pseudo-termp
good-pseudo-term-listp
good-valuep
if-star
ifix
intern-in-package-of-symbol
maybe-natp
maybe-string-fix
mbt-dollar
member-symbol-name
nfix
nibblep
nonkeyword-listp
organize-symbols-by-name
organize-symbols-by-pkg
pos-fix
realfix
rfix
symbol-name-lst
symbol-package-name-lst
symbol-package-name-non-cl
two-nats-measure
other
(in-package "ACL2")
include-book
(include-book "arith-equivs")
include-book
(include-book "bytep")
include-book
(include-book "defs")
include-book
(include-book "fix")
include-book
(include-book "good-pseudo-termp")
include-book
(include-book "good-pseudo-term-listp")
include-book
(include-book "good-valuep")
include-book
(include-book "if-star")
include-book
(include-book "ifix")
include-book
(include-book "intern-in-package-of-symbol")
include-book
(include-book "maybe-natp")
include-book
(include-book "maybe-string-fix")
include-book
(include-book "mbt-dollar")
include-book
(include-book "member-symbol-name")
include-book
(include-book "nfix")
include-book
(include-book "nibblep")
include-book
(include-book "nonkeyword-listp")
include-book
(include-book "organize-symbols-by-name")
include-book
(include-book "organize-symbols-by-pkg")
include-book
(include-book "pos-fix")
include-book
(include-book "realfix")
include-book
(include-book "rfix")
include-book
(include-book "symbol-name-lst")
include-book
(include-book "symbol-package-name-lst")
include-book
(include-book "symbol-package-name-non-cl")
include-book
(include-book "two-nats-measure")
other
(defxdoc std/basic :parents (std) :short "A collection of very basic functions that are occasionally convenient." :long "<p>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.</p>")