On this page:
*STANDARD-CI*
*STANDARD-CO*
*STANDARD-OI*
add-custom-keyword-hint
allocate-fixnum-range
assert-event
boole$
character-alistp
characters
comp
comp-gcl
cw
cw!
defabbrev
defchoose
defcong
defdoc
defevaluator
defexec
define-trusted-clause-processor
defmacro
defn
defpkg
defrefinement
defstobj
defthmd
defttag
defun-sk
defund
e0-ord-<
e0-ordinalp
encapsulate
er
er-progn
error1
evisc-table
flet
fms
fms!
fmt
fmt!
fmt-to-comment-window
fmt1
fmt1!
getenv$
hard-error
illegal
in-arithmetic-theory
kwote
kwote-lst
local
make-event
mbe
mbt
memoize
mod-expt
must-be-equal
mv-nth
open-input-channel-p
open-output-channel-p
peek-char$
pkg-witness
pprogn
print-object$
prog2$
progn
progn!
proofs-co
read-object
redo-flat
remove-custom-keyword-hint
search
set-body
set-bogus-mutual-recursion-ok
setenv$
show-custom-keyword-hint-expansion
standard-co
standard-oi
sys-call
sys-call-status
table
the
unmemoize
value-triple
verify-guards
verify-termination
Version: 4.1.4.3

1.7 Unsupported

The following ACL2 forms are not currently supported by Dracula.

*STANDARD-CI* : t
*STANDARD-CO* : t
*STANDARD-OI* : t
(add-custom-keyword-hint ...)
(allocate-fixnum-range fixnum-lo fixnum-hi)
(assert-event ...)
(boole$ op x y)
(character-alistp any)
(characters any)
(comp ...)
(comp-gcl x)
(cw x)
(cw! x)
(defabbrev ...)
(defchoose ...)
(defcong ...)
(defdoc ...)
(defevaluator ...)
(defexec ...)
(define-trusted-clause-processor ...)
(defmacro ...)
(defn ...)
(defpkg ...)
(defrefinement ...)
(defstobj ...)
(defthmd ...)
(defttag ...)
(defun-sk ...)
(defund ...)
(e0-ord-< a b)
(e0-ordinalp x)
(encapsulate ...)
(er x)
(er-progn ...)
(error1 x)
(evisc-table ...)
(flet (def1 ... defk) body)
(fms ...)
(fms! ...)
(fmt ...)
(fmt! ...)
(fmt-to-comment-window ...)
(fmt1 ...)
(fmt1! ...)
(getenv$ str state)
(hard-error ctx str alist)
(illegal ctx str alist)
(in-arithmetic-theory ...)
(kwote x)
(kwote-lst lst)
(local ...)
(make-event ...)
(mbe ...)
(mbt ...)
(memoize ...)
(mod-expt i j k)
(must-be-equal ...)
(mv-nth n l)
(open-input-channel-p x)
(open-output-channel-p x)
(peek-char$ ...)
(pkg-witness ...)
(pprogn ...)
(print-object$ ...)
(prog2$ x y)
(progn ...)
(progn! ...)
(proofs-co ...)
(read-object ...)
(redo-flat ...)
(remove-custom-keyword-hint ...)
(search x y ...)
(set-body ...)
(set-bogus-mutual-recursion-ok x)
(setenv$ str val)
(show-custom-keyword-hint-expansion ...)
(standard-co ...)
(standard-oi ...)
(sys-call ...)
(sys-call-status ...)
(table ...)
(the ...)
(unmemoize ...)
(value-triple ...)
(verify-guards ...)
(verify-termination ...)