		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Ext-declon-formalp

Check if an external declaration has dynamic formal semantics.

Signature
(ext-declon-formalp edecl) → yes/no
Arguments: edecl — Guard (ext-declonp edecl).
Returns: yes/no — Type (booleanp yes/no).

We support function definitions, function declarations, object declarations, and structure declarations.

Strictly speaking, our current formal dynamic semantics actually ignores all the above except for function definitions: it uses function definitions to build the function environment, but there is no similar function to process the other kinds of external declarations. In theorems generated by ATC, external object and structure types are handled in hypotheses, and function declarations are not used. However, ATC generates the kind of external declarations supported here, so our formal dynamic semantics can (and will) be extended to handle those explicitly. This is why we include them in this predicate.

Definitions and Theorems

Function: ext-declon-formalp

(defun ext-declon-formalp (edecl)
 (declare (xargs :guard (ext-declonp edecl)))
 (declare (xargs :guard (ext-declon-unambp edecl)))
 (let ((__function__ 'ext-declon-formalp))
   (declare (ignorable __function__))
   (ext-declon-case edecl
                    :fundef (fundef-formalp edecl.fundef)
                    :declon (or (declon-obj-formalp edecl.declon)
                                (declon-struct-formalp edecl.declon)
                                (declon-fun-formalp edecl.declon))
                    :empty nil
                    :asm nil)))

Theorem: booleanp-of-ext-declon-formalp

(defthm booleanp-of-ext-declon-formalp
  (b* ((yes/no (ext-declon-formalp edecl)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: ext-declon-formalp-of-ext-declon-fix-edecl

(defthm ext-declon-formalp-of-ext-declon-fix-edecl
  (equal (ext-declon-formalp (ext-declon-fix edecl))
         (ext-declon-formalp edecl)))

Theorem: ext-declon-formalp-ext-declon-equiv-congruence-on-edecl

(defthm ext-declon-formalp-ext-declon-equiv-congruence-on-edecl
  (implies (ext-declon-equiv edecl edecl-equiv)
           (equal (ext-declon-formalp edecl)
                  (ext-declon-formalp edecl-equiv)))
  :rule-classes :congruence)