		Search-engine friendly clone of the ACL2 documentation.

Event-macro-intro-macros

Theorem-intro-macro

Macro (name) for introducing a theorem with a given enablement.

Signature
(theorem-intro-macro enable) → macro
Arguments: enable — Enable theorem or not.
Guard (booleanp enable).
Returns: macro — Type (member-eq macro '(defthm defthmd)).

Definitions and Theorems

Function: theorem-intro-macro

(defun theorem-intro-macro (enable)
       (declare (xargs :guard (booleanp enable)))
       (let ((__function__ 'theorem-intro-macro))
            (declare (ignorable __function__))
            (if enable 'defthm 'defthmd)))

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

(defthm return-type-of-theorem-intro-macro
        (b* ((macro (theorem-intro-macro enable)))
            (member-eq macro '(defthm defthmd)))
        :rule-classes :rewrite)