		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-ident

Check an identifier.

Signature
(check-ident id) → wf?
Arguments: id — Guard (identp id).
Returns: wf? — Type (wellformed-resultp wf?).

We check whether the underlying ACL2 string forms a portable ASCII identifier.

Definitions and Theorems

Function: check-ident

(defun check-ident (id)
  (declare (xargs :guard (identp id)))
  (let ((__function__ 'check-ident))
    (declare (ignorable __function__))
    (if (paident-stringp (ident->name id))
        :wellformed
      (reserrf (list :illegal/unsupported-ident (ident-fix id))))))

Theorem: wellformed-resultp-of-check-ident

(defthm wellformed-resultp-of-check-ident
  (b* ((wf? (check-ident id)))
    (wellformed-resultp wf?))
  :rule-classes :rewrite)

Theorem: check-ident-of-ident-fix-id

(defthm check-ident-of-ident-fix-id
  (equal (check-ident (ident-fix id))
         (check-ident id)))

Theorem: check-ident-ident-equiv-congruence-on-id

(defthm check-ident-ident-equiv-congruence-on-id
  (implies (ident-equiv id id-equiv)
           (equal (check-ident id)
                  (check-ident id-equiv)))
  :rule-classes :congruence)