Include-an-arithmetic-book
Macros for including arithmetic books
| Primitive | Book and Config |
|---|
| arithmetic | arithmetic/top-with-meta |
| arithmetic-5 | arithmetic-5/top |
| arithmetic-5-nonlinear-weak | arithmetic-5/top with weak
nonlinear hint settings |
| arithmetic-5-nonlinear | arithmetic-5/top with stronger
nonlinear hint settings |
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.
