• Top

• Identifiers

Identifier-string-p

Check if a string is a valid Leo identifier.

Signature

(identifier-string-p string) → yes/no

Arguments

string — Guard (stringp string).

Returns

yes/no — Type (booleanp yes/no).

The string's characters must follow the grammar rule. In addition, the string must not be a keyword or boolean literal, and must not be or start with aleo1.

Definitions and Theorems

Function: identifier-string-p

(defun identifier-string-p (string)
  (declare (xargs :guard (stringp string)))
  (let ((__function__ 'identifier-string-p))
    (declare (ignorable __function__))
    (and (identifier-grammar-chars-p (acl2::explode string))
         (not (member-equal (str-fix string)
                            *keywords*))
         (not (equal (str-fix string) "true"))
         (not (equal (str-fix string) "false"))
         (not (prefixp (acl2::explode "aleo1")
                       (acl2::explode string))))))

Theorem: booleanp-of-identifier-string-p

(defthm booleanp-of-identifier-string-p
  (b* ((yes/no (identifier-string-p string)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: identifier-string-p-of-str-fix-string

(defthm identifier-string-p-of-str-fix-string
  (equal (identifier-string-p (str-fix string))
         (identifier-string-p string)))

Theorem: identifier-string-p-streqv-congruence-on-string

(defthm identifier-string-p-streqv-congruence-on-string
  (implies (acl2::streqv string string-equiv)
           (equal (identifier-string-p string)
                  (identifier-string-p string-equiv)))
  :rule-classes :congruence)