Filtering...

symlet

books/tools/symlet

Included Books

bstar
other
(in-package "ACL2")
include-book
(include-book "std/util/bstar" :dir :system)
let-symsmacro
(defmacro let-syms
  (bindings term)
  (sublis (pairlis$ (strip-cars bindings)
      (strip-cars (strip-cdrs bindings)))
    term))
other
(def-b*-binder symlet
  :body (cond ((and (eql (len args) 1) (eql (len forms) 1)) `(let-syms ((,(CAR ARGS) ,(CAR FORMS))) ,REST-EXPR))
    ((and (doublet-listp args) (not forms)) `(let-syms ,ARGS ,REST-EXPR))
    (t (er hard?
        'symlet
        "Symlet takes either exactly 1 argument and 1 ~
                            form, or a doublet-list as arguments and no form"))))