		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Paramdeclor-formalp

Check if a parameter declarator has formal dynamic semantics.

Signature
(paramdeclor-formalp paramdeclor) → yes/no
Arguments: paramdeclor — Guard (paramdeclorp paramdeclor).
Returns: yes/no — Type (booleanp yes/no).

Based on ldm-paramdeclor, the parameter declarator must be present and not abstract. The underlying declarator must be supported, for an object.

Definitions and Theorems

Function: paramdeclor-formalp

(defun paramdeclor-formalp (paramdeclor)
 (declare (xargs :guard (paramdeclorp paramdeclor)))
 (declare (xargs :guard (paramdeclor-unambp paramdeclor)))
 (let ((__function__ 'paramdeclor-formalp))
   (declare (ignorable __function__))
   (paramdeclor-case paramdeclor
                     :declor (declor-obj-formalp paramdeclor.unwrap)
                     :absdeclor nil
                     :none nil
                     :ambig (impossible))))

Theorem: booleanp-of-paramdeclor-formalp

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

Theorem: paramdeclor-formalp-of-paramdeclor-fix-paramdeclor

(defthm paramdeclor-formalp-of-paramdeclor-fix-paramdeclor
  (equal (paramdeclor-formalp (paramdeclor-fix paramdeclor))
         (paramdeclor-formalp paramdeclor)))

Theorem: paramdeclor-formalp-paramdeclor-equiv-congruence-on-paramdeclor

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