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