		Search-engine friendly clone of the ACL2 documentation.

Restrict-input-processing

Restrict-process-undefined

Process the :undefined input.

Signature
(restrict-process-undefined undefined old ctx state) → (mv erp undefined state)
Arguments: old — Guard (symbolp old).
Returns: undefined — A pseudo-termp that is the translation of undefined.

Definitions and Theorems

Function: restrict-process-undefined

(defun restrict-process-undefined (undefined old ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (symbolp old)))
  (let ((__function__ 'restrict-process-undefined))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         ((er (list term stobjs-out))
          (ensure-value-is-untranslated-term$
               undefined "The :UNDEFINED input" t nil))
         (description
              (msg "The term ~x0 that denotes the undefined value"
                   undefined))
         ((er &)
          (ensure-term-free-vars-subset$ term (formals old wrld)
                                         description t nil))
         ((er &)
          (ensure-term-logic-mode$ term description t nil))
         ((er &)
          (ensure-function/lambda/term-number-of-results$
               stobjs-out 1 description t nil))
         ((er &)
          (ensure-term-no-stobjs$ stobjs-out description t nil))
         ((er &)
          (ensure-term-does-not-call$ term old description t nil)))
      (value term))))