		Search-engine friendly clone of the ACL2 documentation.

Template-generators

Template-fn-nonrecursive

Template of a non-recursive function definition.

Signature
(template-fn-nonrecursive fn body arity logic) → fn-def
Arguments: fn — Guard (symbolp fn).; body — Guard (symbolp body).; arity — Guard (natp arity).; logic — Guard (booleanp logic).
Returns: fn-def — Type (pseudo-event-formp fn-def).

This template has the form

(defun fn (x1 ... xn) ; n = arity
  (declare (xargs :mode mode))
  (body x1 ... xn))

Definitions and Theorems

Function: template-fn-nonrecursive

(defun
 template-fn-nonrecursive
 (fn body arity logic)
 (declare (xargs :guard (and (symbolp fn)
                             (symbolp body)
                             (natp arity)
                             (booleanp logic))))
 (let
  ((__function__ 'template-fn-nonrecursive))
  (declare (ignorable __function__))
  (b*
   ((params (template-fn-params arity)))
   (cons
    'progn
    (cons
     (cons 'defstub
           (cons body (cons (repeat arity '*) '(=> *))))
     (cons
      (cons
       'defun
       (cons
        fn
        (cons
         params
         (cons
          (cons
           'declare
           (cons
                (cons 'xargs
                      (cons ':mode
                            (cons (if logic :logic :program) 'nil)))
                'nil))
          (cons (cons body params) 'nil)))))
      'nil))))))

Theorem: pseudo-event-formp-of-template-fn-nonrecursive

(defthm
     pseudo-event-formp-of-template-fn-nonrecursive
     (b* ((fn-def (template-fn-nonrecursive fn body arity logic)))
         (pseudo-event-formp fn-def))
     :rule-classes :rewrite)