Ihs-init
The root of the IHS (Integer Hardware Specification) library hierarchy.
The ihs-init book is included by every book in the IHS
hierarchy. It contains:
- Definitions of CLTL functions that should be part of the ACL2 BOOT-STRAP
theory. Since ACL2 won't let us redefine any Common Lisp symbol, these
functions are uniformly named by <CLTL name>$.
- Functions that are not defined by CLTL, but that are otherwise candidates
for the ACL2 boot-strap theory.
- Unassigned functions that are general purpose, and will probably find a
place in another book someday.
- Definition of macros, macro helper-functions, and utility functions that
are used throughout the IHS libraries. We have no thought of ever verifying
any of these. Thus, the guards of certain functions may be just strong enough
to get the functions admitted.
Subtopics
- Ihs-utilities
- Utility macros and functions used throughout the IHS books.
