Process the inputs.
(print-and-write-files-process-inputs args wrld) → (mv erp tunits)
Function:
(defun print-and-write-files-process-inputs (args wrld) (declare (xargs :guard (and (true-listp args) (plist-worldp wrld)))) (let ((__function__ 'print-and-write-files-process-inputs)) (declare (ignorable __function__)) (b* (((reterr) (transunit-ensemble nil)) ((mv erp extra options) (partition-rest-and-keyword-args args *print-and-write-files-allowed-options*)) ((when erp) (reterr (msg "The inputs must be the options ~&0, ~ but instead they are ~x1." *print-and-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." *print-and-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))) (tunits (acl2::constant-value const wrld)) ((unless (transunit-ensemblep tunits)) (reterr (msg "The value of the ~x0 named constant ~ specified by the :CONST input ~ must satisfy TRANSUNIT-ENSEMBLEP, ~ but instead its value is ~x1." const tunits)))) (retok tunits))))
Theorem:
(defthm transunit-ensemblep-of-print-and-write-files-process-inputs.tunits (b* (((mv acl2::?erp ?tunits) (print-and-write-files-process-inputs args wrld))) (transunit-ensemblep tunits)) :rule-classes :rewrite)