other
(in-package "STD")
other
(include-book "add-io-pairs")
other
(include-book "defaggregate")
other
(include-book "defaggrify-defrec")
other
(include-book "defalist")
other
(include-book "defarbrec")
other
(include-book "defarbrec-doc")
other
(include-book "defconsts")
other
(include-book "defenum")
other
(include-book "deffixer")
other
(include-book "defmacro-plus")
other
(include-book "defmacro-plus-doc")
other
(include-book "defirrelevant")
other
(include-book "deflist")
other
(include-book "defmapappend")
other
(include-book "defmvtypes")
other
(include-book "defprojection")
other
(include-book "define")
other
(include-book "defines")
other
(include-book "define-sk")
other
(include-book "defrule")
other
(include-book "defredundant")
other
(include-book "defsum")
other
(include-book "defval")
other
(include-book "def-bound-theorems")
other
(include-book "defthm-commutative")
other
(include-book "tuple")
other
(include-book "error-value-tuples")
other
(include-book "defund-sk")
other
(include-book "defund-sk-doc")
other
(include-book "deftutorial")
other
(include-book "deftutorial-doc")
other
(include-book "defmax-nat")
other
(include-book "defmax-nat-doc")
other
(include-book "defmin-int")
other
(include-book "defmin-int-doc")
other
(include-book "defmapping")
other
(include-book "defmapping-doc")
other
(include-book "definj")
other
(include-book "definj-doc")
other
(include-book "defsurj")
other
(include-book "defsurj-doc")
other
(include-book "defiso")
other
(include-book "defiso-doc")
other
(defxdoc std/util :parents (std macro-libraries) :short "A macro library that automates defining types, introducing typed functions, mapping over lists, and many other boilerplate tasks." :long "<p>We provide macros for</p> <ol> <li>Introducing data types (recognizers and basic theorems) <ul> <li>simple enumerations (@(see defenum)),</li> <li>record types like @('struct')s in C (@(see defaggregate)),</li> <li>(beta) tagged union / variant / sum types (@(see defsum)),</li> <li>typed lists (@(see deflist)), and</li> <li>typed alists (@(see defalist))</li> </ul></li> <li>Projecting a function across a list and either <ul> <li>cons the results together (@(see defprojection)), or</li> <li>append the results (@(see defmapappend)).</li> </ul></li> <li>Defining functions with documentation and related theorems (@(see define))</li> <li>Writing mutually-recursive functions with induction schemes (@(see defines))</li> <li>Automating other tedious tasks <ul> <li>@(':type-prescription')s for @('mv')-returning functions (@(see defmvtypes))</li> <li>defining simple constants with @(see xdoc) documentation (@(see defval))</li> <li>defining constants that depend on stobjs, with @('mv') support (@(see defconsts))</li> <li>proving rewrite, type prescription, and linear rules about terms in @(tsee natp), @(tsee unsigned-byte-p), and @(tsee signed-byte-p).</li> </ul></li> </ol> <h3>Loading the library</h3> <p>You can load the full library with:</p> @({ (include-book "std/util/top" :dir :system) }) <p>Alternately, you may find it convenient to just load individual books. Each major macro is typically defined in its own book, e.g., you could do:</p> @({ (include-book "std/util/define" :dir :system) (include-book "std/util/defaggregate" :dir :system) (include-book "std/util/deflist" :dir :system) }) <p>Note that unlike many other @(see std) libraries, these macros are defined in the @('STD::') package. This is mainly to avoid name collisions with older macros like @('deflist') from other libraries.</p>")
other
(add-resource-directory "std-util-design-notes" "design-notes")