		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Const-formalp

Check if a constant has formal dynamic semantics.

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

Based on c::eval-const and c::exec-const, only integer constants pass the test.

Definitions and Theorems

Function: const-formalp

(defun const-formalp (const)
  (declare (xargs :guard (constp const)))
  (let ((__function__ 'const-formalp))
    (declare (ignorable __function__))
    (const-case const :int)))

Theorem: booleanp-of-const-formalp

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

Theorem: const-formalp-of-const-fix-const

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

Theorem: const-formalp-const-equiv-congruence-on-const

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