		Search-engine friendly clone of the ACL2 documentation.

Wrap-fn-implementation

Dirdeclor-wrap-fn-make-wrapper

Make the wrapper function direct declarator if the parameter list is supported.

Signature
(dirdeclor-wrap-fn-make-wrapper dirdeclor wrapper-name arg-base-name blacklist) → (mv blacklist found-paramsp can-create-wrapperp dirdeclor$ idents)
Arguments: dirdeclor — Guard (dirdeclorp dirdeclor).; wrapper-name — Guard (identp wrapper-name).; arg-base-name — Guard (identp arg-base-name).; blacklist — Guard (ident-setp blacklist).
Returns: blacklist — Type (ident-setp blacklist).; found-paramsp — Type (booleanp found-paramsp).; can-create-wrapperp — Type (booleanp can-create-wrapperp).; dirdeclor$ — Type (dirdeclorp dirdeclor$).; idents — Type (ident-listp idents).

See declor-wrap-fn-make-wrapper.

Definitions and Theorems

Theorem: true-listp-of-dirdeclor-wrap-fn-make-wrapper.idents

(defthm true-listp-of-dirdeclor-wrap-fn-make-wrapper.idents
  (b* (((mv ?blacklist
            ?found-paramsp ?can-create-wrapperp
            ?dirdeclor$ ?idents)
        (dirdeclor-wrap-fn-make-wrapper
             dirdeclor
             wrapper-name arg-base-name blacklist)))
    (true-listp idents))
  :rule-classes :type-prescription)