		Search-engine friendly clone of the ACL2 documentation.

No-function-definitions-in-dynamic-semantics

Funinfo-nofunp

Check that a function information has no function definitions in the function's body.

Signature
(funinfo-nofunp funinfo) → yes/no
Arguments: funinfo — Guard (funinfop funinfo).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: funinfo-nofunp

(defun funinfo-nofunp (funinfo)
  (declare (xargs :guard (funinfop funinfo)))
  (let ((__function__ 'funinfo-nofunp))
    (declare (ignorable __function__))
    (block-nofunp (funinfo->body funinfo))))

Theorem: booleanp-of-funinfo-nofunp

(defthm booleanp-of-funinfo-nofunp
  (b* ((yes/no (funinfo-nofunp funinfo)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: block-nofunp-of-funinfo->body

(defthm block-nofunp-of-funinfo->body
  (equal (block-nofunp (funinfo->body funinfo))
         (funinfo-nofunp funinfo)))

Theorem: funinfo-nofunp-of-funinfo-fix-funinfo

(defthm funinfo-nofunp-of-funinfo-fix-funinfo
  (equal (funinfo-nofunp (funinfo-fix funinfo))
         (funinfo-nofunp funinfo)))

Theorem: funinfo-nofunp-funinfo-equiv-congruence-on-funinfo

(defthm funinfo-nofunp-funinfo-equiv-congruence-on-funinfo
  (implies (funinfo-equiv funinfo funinfo-equiv)
           (equal (funinfo-nofunp funinfo)
                  (funinfo-nofunp funinfo-equiv)))
  :rule-classes :congruence)