		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Extdecl-formalp

Check if an external declaration has dynamic formal semantics.

Signature
(extdecl-formalp edecl) → yes/no
Arguments: edecl — Guard (extdeclp 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: extdecl-formalp

(defun extdecl-formalp (edecl)
  (declare (xargs :guard (extdeclp edecl)))
  (declare (xargs :guard (extdecl-unambp edecl)))
  (let ((__function__ 'extdecl-formalp))
    (declare (ignorable __function__))
    (extdecl-case edecl
                  :fundef (fundef-formalp edecl.unwrap)
                  :decl (or (decl-obj-formalp edecl.unwrap)
                            (decl-struct-formalp edecl.unwrap)
                            (decl-fun-formalp edecl.unwrap))
                  :empty nil
                  :asm nil)))

Theorem: booleanp-of-extdecl-formalp

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

Theorem: extdecl-formalp-of-extdecl-fix-edecl

(defthm extdecl-formalp-of-extdecl-fix-edecl
  (equal (extdecl-formalp (extdecl-fix edecl))
         (extdecl-formalp edecl)))

Theorem: extdecl-formalp-extdecl-equiv-congruence-on-edecl

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