		Search-engine friendly clone of the ACL2 documentation.

Modname

Modname-p

Signature
(modname-p x) → *

Definitions and Theorems

Function: modname-p

(defun modname-p (x)
  (declare (ignorable x))
  (declare (xargs :guard t))
  (let ((__function__ 'modname-p))
    (declare (ignorable __function__))
    (not (eq x nil))))

Theorem: modname-p-booleanp

(defthm modname-p-booleanp
  (booleanp (modname-p x))
  :rule-classes :type-prescription)

Theorem: modname-p-compound-recognizer

(defthm modname-p-compound-recognizer
  (implies (modname-p x) x)
  :rule-classes :compound-recognizer)