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