		Search-engine friendly clone of the ACL2 documentation.

Defisar-implementation

Defisar-fn

Generate and submit the defisar events.

Signature
(defisar-fn name formula proof disable rule-classes ctx state) → (mv erp event state)
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: defisar-fn

(defun defisar-fn (name formula
                        proof disable rule-classes ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defisar-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp name))
     (er-soft+
      ctx t '(_)
      "The name input must be a symbol, ~
                   but it is ~x0 instead."
      name))
    ((unless (true-listp proof))
     (er-soft+
      ctx t '(_)
      "The :PROOF input must be a list of commands, ~
                   but it is ~x0 instead."
      proof))
    ((unless (booleanp disable))
     (er-soft+
      ctx t '(_)
      "The :DISABLE input must be a boolean, ~
                   but it is ~x0 instead."
      disable))
    ((mv erp events state)
     (defisar-proof proof name
                    formula disable rule-classes ctx state))
    ((when erp) (mv erp '(_) state)))
   (value (cons 'progn
                (cons (cons 'encapsulate
                            (cons 'nil
                                  (cons '(set-ignore-ok t) events)))
                      '((value-triple :invisible))))))))

Theorem: pseudo-event-formp-of-defisar-fn.event

(defthm pseudo-event-formp-of-defisar-fn.event
  (b* (((mv ?erp acl2::?event acl2::?state)
        (defisar-fn name formula
                    proof disable rule-classes ctx state)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)