		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Defarbrec-process-nonterminating

Process the :nonterminating input.

Signature
(defarbrec-process-nonterminating nonterminating x1...xn$ ctx state) → (mv erp nonterminating$ state)
Arguments: x1...xn$ — Guard (symbol-listp x1...xn$).
Returns: nonterminating$ — A pseudo-termp.

Return the translated form of the term.

Note that the check that the term calls only logic-mode functions ensures that the term does not call the program-mode function fn.

Definitions and Theorems

Function: defarbrec-process-nonterminating

(defun defarbrec-process-nonterminating
       (nonterminating x1...xn$ ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (symbol-listp x1...xn$)))
 (let ((__function__ 'defarbrec-process-nonterminating))
   (declare (ignorable __function__))
   (b*
     (((er (list term stobjs-out))
       (ensure-value-is-untranslated-term$
            nonterminating
            "The :NONTERMINATING input" t nil))
      (description
           (msg "The term ~x0 supplied as the :NONTERMINATING input"
                nonterminating))
      ((er &)
       (ensure-term-free-vars-subset$
            term x1...xn$ 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)))
     (value term))))