		Search-engine friendly clone of the ACL2 documentation.

Event-macro-intro-macros

Function-intro-macro

Macro (name) for introducing a function with given enablement and non-executability.

Signature
(function-intro-macro enable non-executable) → macro
Arguments: enable — Enable function or not.
Guard (booleanp enable).; non-executable — Make function non-executable or not.
Guard (booleanp non-executable).
Returns: macro — Type (member-eq macro '(defun defund defun-nx defund-nx)).

Definitions and Theorems

Function: function-intro-macro

(defun function-intro-macro (enable non-executable)
  (declare (xargs :guard (and (booleanp enable)
                              (booleanp non-executable))))
  (let ((__function__ 'function-intro-macro))
    (declare (ignorable __function__))
    (if enable (if non-executable 'defun-nx 'defun)
      (if non-executable 'defund-nx
        'defund))))

Theorem: return-type-of-function-intro-macro

(defthm return-type-of-function-intro-macro
  (b* ((macro (function-intro-macro enable non-executable)))
    (member-eq macro
               '(defun defund defun-nx defund-nx)))
  :rule-classes :rewrite)