top

(in-package "ACL2")

(defsection std
  :parents (top)
  :short "Standard libraries for ACL2."
  :long "<p>The <b>std</b> library is meant to become <i>ACL2, Batteries
Included</i>.  Its features a wide variety of books that work well together to
provide a well-thought-out, documented, coherent reasoning strategy.</p>

<p>@('Std') is currently under active development.  You are welcome to use it,
but please be aware that things may change out from under you.</p>

<p>So far, @('std') itself includes libraries about
   <see topic='@(url std/basic)'>basic</see> concepts,
   <see topic='@(url std/lists)'>lists</see>,
   <see topic='@(url std/osets)'>sets</see>,
   <see topic='@(url std/alists)'>alists</see>,
   <see topic='@(url std/typed-lists)'>typed-lists</see>,
   <see topic='@(url acl2::std/stobjs)'>stobjs</see>,
   <see topic='@(url std/io)'>input/output</see>.
Each of these libraries provides many lemmas for reasoning about built-in
ACL2 functions, and also many additional functions.  There is also a very
convenient @(see std/util) macro library, with macros that automate many
otherwise-tedious tasks.  There is also a @(see std/testing) library with
utilities to create tests.</p>")