		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)