		Search-engine friendly clone of the ACL2 documentation.

Input-processing

Process-const-new

Process the :const-new input of a transformation.

Signature
(process-const-new const-new suppliedp) → (mv erp const-new)
Arguments: suppliedp — Guard (booleanp suppliedp).
Returns: const-new — Type (symbolp const-new).

We check that the input was supplied and that it is a symbol. For now we do not check that it is a fresh constant name not already present in the world, but we may extend this function to do that. We return the input unchanged if successful, but with a stronger type provided by the return theorem.

Definitions and Theorems

Function: process-const-new

(defun process-const-new (const-new suppliedp)
 (declare (xargs :guard (booleanp suppliedp)))
 (let ((__function__ 'process-const-new))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((unless suppliedp)
     (reterr (msg "The :CONST-NEW input must be supplied.")))
    ((unless (symbolp const-new))
     (reterr
      (msg
       "The :CONST-NEW must be a symbol, ~
                      but it is ~x0 instead."
       const-new))))
   (retok const-new))))

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

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