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
defequiv
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

2.6 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 ...)

(defequiv ...)

(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 ...)