other
(in-package "ACL2S")
other
(include-book "defdata/top" :ttags :all)
other
(include-book "std/lists/top" :dir :system)
other
(include-book "std/alists/top" :dir :system)
other
(include-book "ordinals/lexicographic-ordering-without-arithmetic" :dir :system)
other
(include-book "misc/meta-lemmas" :dir :system)
other
(include-book "std/testing/eval" :dir :system)
other
(include-book "tau/bounders/elementary-bounders" :dir :system)
other
(include-book "utilities")
other
(include-book "definec" :ttags :all)
other
(include-book "cons-size")
other
(include-book "properties")
other
(include-book "base-properties")
other
(include-book "check-equal")
other
(include-book "std/strings/top" :dir :system)
other
(include-book "system/doc/developers-guide" :dir :system)
other
(include-book "acl2s/acl2s-size" :dir :system)
other
(include-book "acl2s/ccg/ccg" :dir :system :uncertified-okp nil :ttags ((:ccg)) :load-compiled-file nil)
other
(include-book "base-arithmetic" :ttags :all)
other
(include-book "base-lists" :ttags :all)
other
(include-book "acl2s/cgen/base-cgen-rules" :dir :system)
other
(include-book "match" :ttags :all)
other
(include-book "kestrel/utilities/ubi" :dir :system)
other
(set-termination-method :ccg)
other
(local (set-defunc-timeout 1000))
other
(make-event (er-progn (set-ccg-inhibit-output-lst *ccg-valid-output-names*) (value '(value-triple :invisible))))