		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-fn

Process the fn input.

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

Definitions and Theorems

Function: defarbrec-process-fn

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

Theorem: null-of-defarbrec-process-fn.nothing

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