		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-process-const

Process the :const inputs.

Signature
(input-files-process-const const-presentp const progp) → (mv erp new-const)
Arguments: const-presentp — Guard (booleanp const-presentp).; progp — Guard (booleanp progp).
Returns: new-const — Type (symbolp new-const).

If the programmatic interface has been called, this input must be absent. In this case, we return nil as result.

Definitions and Theorems

Function: input-files-process-const

(defun input-files-process-const (const-presentp const progp)
 (declare (xargs :guard (and (booleanp const-presentp)
                             (booleanp progp))))
 (let ((__function__ 'input-files-process-const))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when progp)
     (b*
      (((when const-presentp)
        (reterr
         (msg
          "The :CONST input must not be supplied ~
                            to the programmatic interface."))))
      (retok nil)))
    ((unless const-presentp)
     (reterr
      (msg
       "The :CONST input must be supplied, ~
                      but it was not supplied.")))
    ((unless (symbolp const))
     (reterr
      (msg
       "The :CONST input must be a symbol, ~
                      but it is ~x0 instead."
       const))))
   (retok const))))

Theorem: symbolp-of-input-files-process-const.new-const

(defthm symbolp-of-input-files-process-const.new-const
  (b* (((mv acl2::?erp ?new-const)
        (input-files-process-const const-presentp const progp)))
    (symbolp new-const))
  :rule-classes :rewrite)