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
defttag
defun-sk
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

1.7 Unsupported

The following ACL2 forms are not currently supported by Dracula.

value

*STANDARD-CI* : t

value

*STANDARD-CO* : t

value

*STANDARD-OI* : t

syntax

(add-custom-keyword-hint ...)

syntax

(allocate-fixnum-range fixnum-lo fixnum-hi)

syntax

(assert-event ...)

syntax

(boole$ op x y)

syntax

(character-alistp any)

syntax

(characters any)

syntax

(comp ...)

syntax

(comp-gcl x)

syntax

(cw x)

syntax

(cw! x)

syntax

(defabbrev ...)

syntax

(defchoose ...)

syntax

(defcong ...)

syntax

(defdoc ...)

syntax

(defevaluator ...)

syntax

(defexec ...)

syntax

(define-trusted-clause-processor ...)

syntax

(defmacro ...)

syntax

(defn ...)

syntax

(defpkg ...)

syntax

(defrefinement ...)

syntax

(defstobj ...)

syntax

(defttag ...)

syntax

(defun-sk ...)

syntax

(e0-ord-< a b)

syntax

(e0-ordinalp x)

syntax

(encapsulate ...)

syntax

(er x)

syntax

(er-progn ...)

syntax

(error1 x)

syntax

(evisc-table ...)

syntax

(flet (def1 ... defk) body)

syntax

(fms ...)

syntax

(fms! ...)

syntax

(fmt ...)

syntax

(fmt! ...)

syntax

(fmt-to-comment-window ...)

syntax

(fmt1 ...)

syntax

(fmt1! ...)

syntax

(getenv$ str state)

syntax

(hard-error ctx str alist)

syntax

(illegal ctx str alist)

syntax

(in-arithmetic-theory ...)

syntax

(kwote x)

syntax

(kwote-lst lst)

syntax

(local ...)

syntax

(make-event ...)

syntax

(mbe ...)

syntax

(mbt ...)

syntax

(memoize ...)

syntax

(mod-expt i j k)

syntax

(must-be-equal ...)

syntax

(mv-nth n l)

syntax

(open-input-channel-p x)

syntax

(open-output-channel-p x)

syntax

(peek-char$ ...)

syntax

(pkg-witness ...)

syntax

(pprogn ...)

syntax

(print-object$ ...)

syntax

(prog2$ x y)

syntax

(progn ...)

syntax

(progn! ...)

syntax

(proofs-co ...)

syntax

(read-object ...)

syntax

(redo-flat ...)

syntax

(remove-custom-keyword-hint ...)

syntax

(search x y ...)

syntax

(set-body ...)

syntax

(set-bogus-mutual-recursion-ok x)

syntax

(setenv$ str val)

syntax

(show-custom-keyword-hint-expansion ...)

syntax

(standard-co ...)

syntax

(standard-oi ...)

syntax

(sys-call ...)

syntax

(sys-call-status ...)

syntax

(table ...)

syntax

(the ...)

syntax

(unmemoize ...)

syntax

(value-triple ...)

syntax

(verify-guards ...)

syntax

(verify-termination ...)