		Search-engine friendly clone of the ACL2 documentation.

Solve-input-processing

Solve-process-solution-enable

Process the :solution-enable input.

Signature
(solve-process-solution-enable solution-enable solution-enable? f-existsp ctx state) → (mv erp nothing state)
Arguments: solution-enable? — Guard (booleanp solution-enable?).; f-existsp — Guard (booleanp f-existsp).
Returns: nothing — Type (null nothing).

Definitions and Theorems

Function: solve-process-solution-enable

(defun solve-process-solution-enable
       (solution-enable solution-enable? f-existsp ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (booleanp solution-enable?)
                             (booleanp f-existsp))))
 (let ((__function__ 'solve-process-solution-enable))
  (declare (ignorable __function__))
  (if
   (and solution-enable? f-existsp)
   (er-soft+
    ctx t nil
    "Since the :SOLUTION-name input ~
                 specifies an existing function, ~
                 the :SOLUTION-ENABLE input must be absent.")
   (ensure-value-is-boolean$ solution-enable
                             "The :SOLUTION-ENABLE input" t nil))))

Theorem: null-of-solve-process-solution-enable.nothing

(defthm null-of-solve-process-solution-enable.nothing
  (b* (((mv ?erp ?nothing acl2::?state)
        (solve-process-solution-enable
             solution-enable
             solution-enable? f-existsp ctx state)))
    (null nothing))
  :rule-classes :rewrite)