/usr/share/acl2-4.3/books/str/doc.lisp is in acl2-books-source 4.3-3.
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 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 | ; ACL2 String Library
; Copyright (C) 2009-2010 Centaur Technology
;
; Contact:
; Centaur Technology Formal Verification Group
; 7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
; http://www.centtech.com/
;
; This program is free software; you can redistribute it and/or modify it under
; the terms of the GNU General Public License as published by the Free Software
; Foundation; either version 2 of the License, or (at your option) any later
; version. This program is distributed in the hope that it will be useful but
; WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
; more details. You should have received a copy of the GNU General Public
; License along with this program; if not, write to the Free Software
; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335, USA.
;
; Original author: Jared Davis <jared@centtech.com>
(in-package "STR")
(defdoc Str
":Doc-Section Str
ACL2 String Library~/
This is a rudimentary string library for ACL2. The functions here are all in
logic mode, with verified guards. Effort has been spent to make them both
reasonably efficient and relatively straightforward to reason about. Note that
since we make extensive use of MBE, you will need to verify your own functions'
guards in order to get good performance out of most library functions.
LOADING, DOCUMENTATION.
Ordinarily, to use the library one should run
~bv[]
(include-book \"str/top\" :dir :system)
~ev[]
The documentation is then available by writing ~c[:doc STR::str]. All of the
library's functions are found in the STR package, so you will need to do one of
the following.
1. Type STR:: before the names of the functions, OR
2. Additionally load a set of ACL2-package macros which are aliases for the
functions in the STR package. To do this, run:
~c[(include-book \"str/abbrevs\" :dir :system)]
LIBRARY FUNCTIONS.
There are probably many things to add. For now, here are the functions which
are available.
~/
LICENSE.
This program is free software; you can redistribute it and/or modify it under
the terms of the GNU General Public License as published by the Free Software
Foundation; either version 2 of the License, or (at your option) any later
version. This program is distributed in the hope that it will be useful but
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
more details. You should have received a copy of the GNU General Public
License along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.")
|