Write-list
Write a list to a file
Example Forms:
(write-list '(a b c) "foo" 'top-level state)
(write-list '(a b c) "foo" 'top-level state :quiet t)
General Form:
(write-list list x ctx state &key :quiet val)
where all arguments are evaluated and state must literally be the ACL2
state, STATE. List is a true-list; x is a filename or a
list of length 1 containing a filename; and ctx is a context (see ctx). By default or if :quiet is nil, a message of the form "Writing
file [x]" is printed to standard-co; otherwise, no such message is
printed.
Also see print-object$ and print-object$+.
