include-an-arithmetic-book

Included Books

top

other

(in-package "ACL2")

include-book

(include-book "xdoc/top" :dir :system)

other

(defxdoc include-an-arithmetic-book
  :parents (arithmetic)
  :short "Macros for including arithmetic books"
  :long "<table>
 <tr><th>Primitive</th><th>Book and Config</th></tr>
 <tr><td>@('arithmetic')</td><td>@('arithmetic/top-with-meta')</td></tr>
 <tr><td>@('arithmetic-5')</td><td>@('arithmetic-5/top')</td></tr>
 <tr><td>@('arithmetic-5-nonlinear-weak')</td><td>@('arithmetic-5/top') with weak
      nonlinear hint settings</td></tr>
 <tr><td>@('arithmetic-5-nonlinear')</td><td>@('arithmetic-5/top') with stronger
      nonlinear hint settings</td></tr>
 </table>

 Note that it can be reasonable to only include this book locally, since these
 forms can often only occur in lemmas local to the book performing the
 including.")

arithmeticmacro

(defmacro arithmetic
  nil
  `(include-book "arithmetic/top-with-meta" :dir :system))

arithmetic-5macro

(defmacro arithmetic-5
  nil
  `(include-book "arithmetic-5/top" :dir :system))

arithmetic-5-nonlinear-weakmacro

(defmacro arithmetic-5-nonlinear-weak
  nil
  '(progn (include-book "arithmetic-5/top" :dir :system)
    (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
         hist
         pspv)))))

arithmetic-5-nonlinearmacro

(defmacro arithmetic-5-nonlinear
  nil
  '(progn (include-book "arithmetic-5/top" :dir :system)
    (set-default-hints '((nonlinearp-default-hint++ id
         stable-under-simplificationp
         hist
         nil)))))