/usr/share/hol88-2.02.19940316/help/ENTRIES/lisp.doc is in hol88-help 2.02.19940316-35.
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 | \DOC lisp
\TYPE {lisp : (string -> void)}
\SYNOPSIS
Executes a lisp command from ML.
\DESCRIBE
{lisp} executes a lisp s-expression (written as an ML string). Returned
values do not appear on the standard output, unless they are explicitly
printed.
\FAILURE
Fails if the s-expression is improperly constructed or fails when
evaluated by lisp.
\EXAMPLE
{
#lisp `(princ "hello")`;;
hello() : void
#lisp `(cons 'a 'b)`;;
() : void
#lisp `(princ (cons 'a 'b))`;;
(A . B)() : void
#lisp `(car 'a)`;;
Error: Attempt to take the car of A which is not a cons.
evaluation failed lisp -- NIL
#lisp `(princ "hello"`;;
Error: eof encountered on input stream #<string input stream @ #x869fe6>
evaluation failed lisp -- NIL
}
\COMMENTS
{lisp} is not meant for general use, and should be treated with great
care. If one is not wary, it is entirely possible to corrupt HOL by
using it.
\SEEALSO
dropout, lsp.
\ENDDOC
|