		Search-engine friendly clone of the ACL2 documentation.

Defmapping-input-processing

Defmapping-process-name

Process the name input.

Signature
(defmapping-process-name name ctx state) → (mv erp nothing state)
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: defmapping-process-name

(defun defmapping-process-name (name ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defmapping-process-name))
   (declare (ignorable __function__))
   (b* (((er &)
         (ensure-value-is-symbol$ name "The first input" t nil))
        ((er &)
         (ensure-symbol-not-keyword$ name "The first input" t nil)))
     (value nil))))

Theorem: null-of-defmapping-process-name.nothing

(defthm null-of-defmapping-process-name.nothing
  (b* (((mv ?erp ?nothing ?state)
        (defmapping-process-name name ctx state)))
    (null nothing))
  :rule-classes :rewrite)