Filtering...

defunc-testing

books/acl2s/defunc-testing
other
(in-package "ACL2S")
other
(include-book "acl2s/ccg/ccg" :uncertified-okp nil :dir :system :ttags ((:ccg)) :load-compiled-file nil)
other
(include-book "acl2s/base-theory" :dir :system :ttags :all)
other
(include-book "acl2s/custom" :dir :system :ttags :all)
other
(include-book "acl2s/acl2s-sigs" :dir :system :ttags :all)
other
(include-book "acl2s/definec" :dir :system :ttags :all)
other
(set-well-founded-relation l<)
other
(set-termination-method :ccg)
other
(set-ccg-time-limit 300)
other
(definec d-t1 (x :int) :int x)
other
(definec d-t1 (x :int) :int x)
other
(property (x :int)
  (== (d-t1 x) x))
other
(property d-t1-thm
  (x :int)
  (== (d-t1 x) x))
other
(definec foo
  (x y :int z :tl :cons)
  :cons (if (< x y)
    z
    (foo (- x 2) (1- y) z)))
other
(definec m4
  (x :rational)
  :nat (abs (ceiling (* x 2) 1)))