Filtering...

bind-macro-args

books/system/bind-macro-args

Included Books

pseudo-good-worldp verified-termination-and-guards kestrel symbol-alistp keyword-value-lists2 assoc-keyword intern-in-package-of-symbol member-symbol-name chk-length-and-keys
other
(in-package "ACL2")
include-book
(include-book "pseudo-good-worldp")
include-book
(include-book "verified-termination-and-guards")
include-book
(include-book "kestrel")
other
(verify-termination warning-off-p1)
other
(verify-termination warning1-cw)
other
(verify-termination duplicate-keys-action)
local
(local (defthm keyword-value-listp-remove-keyword
    (implies (keyword-value-listp x)
      (keyword-value-listp (remove-keyword key x)))))
local
(local (defthm keyword-value-listp-cddr-assoc-keyword
    (implies (keyword-value-listp x)
      (keyword-value-listp (cddr (assoc-keyword key x))))))
other
(verify-termination bind-macro-args-keys1
  (declare (xargs :measure (acl2-count args) :verify-guards nil)))
other
(verify-termination chk-length-and-keys)
other
(verify-termination bind-macro-args-keys
  (declare (xargs :verify-guards nil)))
other
(verify-termination bind-macro-args-after-rest
  (declare (xargs :verify-guards nil)))
other
(verify-termination bind-macro-args-optional
  (declare (xargs :measure (acl2-count args) :verify-guards nil)))
other
(verify-termination bind-macro-args1
  (declare (xargs :measure (acl2-count args) :verify-guards nil)))
other
(verify-termination bind-macro-args
  (declare (xargs :verify-guards nil)))
local
(local (include-book "kestrel/alists-light/symbol-alistp" :dir :system))
local
(local (include-book "kestrel/utilities/keyword-value-lists2" :dir :system))
local
(local (include-book "kestrel/utilities/assoc-keyword" :dir :system))
local
(local (include-book "kestrel/utilities/intern-in-package-of-symbol" :dir :system))
local
(local (include-book "kestrel/utilities/member-symbol-name" :dir :system))
local
(local (include-book "kestrel/utilities/chk-length-and-keys" :dir :system))
local
(local (in-theory (disable true-listp
      macro-arglist-keysp
      plist-worldp
      symbol-alistp
      keyword-value-listp
      fgetprop
      assoc-keyword
      macro-arglist-optionalp
      chk-length-and-keys
      weak-state-vars-p
      table-alist
      mv-nth
      macro-arglist1p
      macro-arglist-optionalp)))
other
(verify-guards bind-macro-args-keys1
  :hints (("Goal" :do-not '(generalize eliminate-destructors)
     :in-theory (enable (:d macro-arglist-keysp)))))
other
(verify-guards bind-macro-args-keys)
other
(verify-guards bind-macro-args-after-rest)
other
(verify-guards bind-macro-args-optional
  :hints (("Goal" :in-theory (enable (:d macro-arglist-optionalp)))))
other
(verify-guards bind-macro-args1
  :hints (("Goal" :expand ((macro-arglist1p args)))))
other
(verify-guards bind-macro-args)