		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-f

Generate the f function.

Signature
(solve-gen-f f x1...xn f-body solution-guard solution-guard-hints solution-enable verify-guards wrld) → (mv local-event exported-event)
Arguments: f — Guard (symbolp f).; x1...xn — Guard (symbol-listp x1...xn).; f-body — Guard (pseudo-termp f-body).; solution-guard — An untranslated term.; solution-guard-hints — Guard (true-listp solution-guard-hints).; solution-enable — Guard (booleanp solution-enable).; verify-guards — Guard (booleanp verify-guards).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.; exported-event — A pseudo-event-formp.

Definitions and Theorems

Function: solve-gen-f

(defun solve-gen-f (f x1...xn f-body
                      solution-guard solution-guard-hints
                      solution-enable verify-guards wrld)
  (declare (xargs :guard (and (symbolp f)
                              (symbol-listp x1...xn)
                              (pseudo-termp f-body)
                              (true-listp solution-guard-hints)
                              (booleanp solution-enable)
                              (booleanp verify-guards)
                              (plist-worldp wrld))))
  (let ((__function__ 'solve-gen-f))
    (declare (ignorable __function__))
    (evmac-generate-defun f
                          :formals x1...xn
                          :body (untranslate f-body nil wrld)
                          :enable solution-enable
                          :guard solution-guard
                          :guard-hints solution-guard-hints
                          :verify-guards verify-guards)))