		Search-engine friendly clone of the ACL2 documentation.

Event-macro-event-generators

Evmac-generate-soft-defunvar

Generate a SOFT function variable with specified name and arity.

Signature
(evmac-generate-soft-defunvar name arity) → event
Arguments: name — Guard (symbolp name).; arity — Guard (natp arity).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: evmac-generate-soft-defunvar

(defun evmac-generate-soft-defunvar (name arity)
  (declare (xargs :guard (and (symbolp name) (natp arity))))
  (let ((__function__ 'evmac-generate-soft-defunvar))
    (declare (ignorable __function__))
    (cons 'soft::defunvar
          (cons name
                (cons (repeat arity '*) '(=> *))))))

Theorem: pseudo-event-formp-of-evmac-generate-soft-defunvar

(defthm pseudo-event-formp-of-evmac-generate-soft-defunvar
  (b* ((event (evmac-generate-soft-defunvar name arity)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)