Declor-wrap-fn-make-wrapper
Make the wrapper function declarator if the parameter list is
supported.
- Signature
(declor-wrap-fn-make-wrapper declor
wrapper-name arg-base-name blacklist)
→
(mv blacklist found-paramsp can-create-wrapperp declor$ idents)- Arguments
- declor — Guard (declorp declor).
- 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).
- declor$ — Type (declorp declor$).
- idents — Type (ident-listp idents).
Also returns an updated blacklist and identifier list corresponding to
the parameters.
The found-paramsp return value is t iff function parameters
were found, as expected. The can-create-wrapperp return is t
iff the parameter list was in the supported set.
Definitions and Theorems
Theorem: true-listp-of-declor-wrap-fn-make-wrapper.idents
(defthm true-listp-of-declor-wrap-fn-make-wrapper.idents
(b* (((mv ?blacklist ?found-paramsp
?can-create-wrapperp ?declor$ ?idents)
(declor-wrap-fn-make-wrapper
declor
wrapper-name arg-base-name blacklist)))
(true-listp idents))
:rule-classes :type-prescription)
