		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Param-declor-formalp

Check if a parameter declarator has formal dynamic semantics.

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

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

Definitions and Theorems

Function: param-declor-formalp

(defun param-declor-formalp (paramdeclor)
  (declare (xargs :guard (param-declorp paramdeclor)))
  (declare (xargs :guard (param-declor-unambp paramdeclor)))
  (let ((__function__ 'param-declor-formalp))
    (declare (ignorable __function__))
    (param-declor-case
         paramdeclor
         :nonabstract (declor-obj-formalp paramdeclor.declor)
         :abstract nil
         :none nil
         :ambig (impossible))))

Theorem: booleanp-of-param-declor-formalp

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

Theorem: param-declor-formalp-of-param-declor-fix-paramdeclor

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

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

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