		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-method-rules

Process the :method-rules input.

Signature
(solve-process-method-rules method-rules ctx state) → (mv erp nothing state)
Returns: nothing — Type (null nothing).

For now we just check that it is a true list of symbols, but give this its own input processing function so that we may add further checks in the future.

Definitions and Theorems

Function: solve-process-method-rules

(defun solve-process-method-rules (method-rules ctx state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'solve-process-method-rules))
    (declare (ignorable __function__))
    (ensure-value-is-symbol-list$ method-rules
                                  "The :METHOD-RULES input" t nil)))

Theorem: null-of-solve-process-method-rules.nothing

(defthm null-of-solve-process-method-rules.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (solve-process-method-rules method-rules ctx state)))
    (null nothing))
  :rule-classes :rewrite)