		Search-engine friendly clone of the ACL2 documentation.

B*-binders

Patbind-access

b* binder for accessing record structure fields introduced with ACL2's defrec.

This is a b* binder introduced with def-b*-binder.

Macro: patbind-access

(defmacro patbind-access (args forms rest-expr)
  (cons 'b*
        (cons (access-b*-bindings (car args)
                                  (car forms)
                                  (cdr args))
              (cons rest-expr 'nil))))