/usr/share/acl2-6.5/books/ihs/ihs-doc-topic.lisp is in acl2-books-source 6.5-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 | ; ihs-doc-topic.lisp -- root of the IHS libraries
; Copyright (C) 1997 Computational Logic, Inc.
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
; [Jared]: I split this out of ihs-init.lisp into its own book so that
; basic-definitions.lisp doesn't need to include ihs-init.lisp
(in-package "ACL2")
(defdoc ihs
":Doc-Section ihs
The Integer Hardware Specification (IHS) library is a collection of
arithmetic books, mainly geared toward bit-vector arithmetic.~/
This is a classic ACL2 arithmetic library wherein bit-vectors are represented
as ordinary ACL2 integers, which has some nice efficiency properties.
Despite the underlying integer-based representation, the library allows you to
easily treat integers akin to lsb-first lists of bits, with the functions
~ilc[logcar] and ~ilc[logcdr] acting as analogues for ~ilc[car] and ~ilc[cdr].
To help you make use of this view, the library introduces alternate,
list-style, recursive definitions for operations like ~ilc[logand]. Once you
understand how to induct in the right way to use these definitions, it becomes
an extremely useful way to prove theorems about these bit functions.
The IHS library is found in:
~bv[]
books/ihs/*.lisp
~ev[]~/~/")
|