Included Books
other
(in-package "ACL2")
include-book
(include-book "serialize-tests")
local
(local (value-triple (cw "Blah is ~x0.~%" "blah")))
local
(local (value-triple (cw "Blah is also ~x0.~%" (hons-copy "blah"))))
local
(local (set-slow-alist-action :break))
other
(value-triple (hons-get '1 *foo*))
other
(value-triple (hons-get "blah" *foo2*))
other
(value-triple (hons-get (concatenate 'string "bl" "ah") *foo2*))
other
(value-triple (hons-get "black" *foo2*))
other
(value-triple (hons-get (concatenate 'string "bl" "ack") *foo2*))
other
(value-triple (hons-get "sheep" *foo2*))
local
(local (set-slow-alist-action :warning))
other
(value-triple (hons-get '1 *bar*))