Filtering...

kestrel

books/system/kestrel

Included Books

verified-termination-and-guards subcor-var aset1 dimensions compress1
other
(in-package "ACL2")
include-book
(include-book "verified-termination-and-guards")
other
(verify-termination def-body)
other
(verify-termination latest-body)
other
(verify-guards latest-body)
other
(verify-termination body)
other
(verify-termination logical-namep)
other
(verify-termination stobjs-out)
other
(verify-termination macro-args)
other
(verify-termination signature-fns)
other
(verify-termination access-event-tuple-namex)
other
(verify-termination termify-clause-set
  (declare (xargs :verify-guards nil)))
other
(verify-guards termify-clause-set)
other
(verify-termination formalized-varlistp)
other
(verify-termination throw-nonexec-error-p1)
other
(verify-termination throw-nonexec-error-p)
other
(verify-termination stobjp)
other
(verify-termination compute-stobj-flags)
other
(verify-termination defun-mode)
other
(verify-termination doublet-listp)
other
(verify-termination implicate)
other
(verify-termination add-suffix-to-fn)
include-book
(include-book "subcor-var")
other
(verify-termination fsubcor-var)
other
(verify-termination get-brr-local)
other
(verify-termination ens-maybe-brr)
other
(verify-termination the-live-var)
other
(verify-termination logical-name-type)
other
(verify-termination new-namep)
other
(verify-termination chk-all-but-new-name-cmp)
other
(verify-termination attach-stobj-guard-msg)
other
(verify-termination attach-stobj-guard)
other
(verify-termination partition-rest-and-keyword-args1)
other
(verify-termination partition-rest-and-keyword-args2)
other
(verify-termination partition-rest-and-keyword-args)
encapsulate
(encapsulate nil
  (local (include-book "kestrel/acl2-arrays/aset1" :dir :system))
  (local (include-book "kestrel/acl2-arrays/dimensions" :dir :system))
  (local (include-book "kestrel/acl2-arrays/compress1" :dir :system))
  (local (in-theory (disable array1p)))
  (verify-termination aset1-lst))