Process the inputs.
(write-files-process-inputs args wrld) → (mv erp fileset)
Function:
(defun write-files-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'write-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) (fileset nil)) ((mv erp extra options) (partition-rest-and-keyword-args args *write-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *write-files-allowed-options* args))) ((when extra) (reterr (msg "The only allowed inputs are the options ~&0, ~ but instead the extra inputs ~x1 were supplied." *write-files-allowed-options* extra))) (const-option (assoc-eq :const options)) ((unless const-option) (reterr (msg "The :CONST input must be supplied, ~ but it was not supplied."))) (const (cdr const-option)) ((unless (symbolp const)) (reterr (msg "The :CONST input must be a symbol, ~ but it is ~x0 instead." const))) (fileset (acl2::constant-value const wrld)) ((unless (filesetp fileset)) (reterr (msg "The value of the ~x0 named constant ~ specified by the :CONST input ~ must satisfy FILESETP, ~ but instead its value is ~x1." const fileset)))) (retok fileset))))
Theorem:
(defthm filesetp-of-write-files-process-inputs.fileset (b* (((mv acl2::?erp ?fileset) (write-files-process-inputs args wrld))) (filesetp fileset)) :rule-classes :rewrite)