		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Plexeme-tokenp

Check if a preprocessing lexeme is a token.

Signature
(plexeme-tokenp lexeme) → yes/no
Arguments: lexeme — Guard (plexemep lexeme).
Returns: yes/no — Type (booleanp yes/no).

This is according to the grammar rule for preprocessing-token [C17:6.4] [C17:A.1.1].

Definitions and Theorems

Function: plexeme-tokenp

(defun plexeme-tokenp (lexeme)
  (declare (xargs :guard (plexemep lexeme)))
  (and (member-eq (plexeme-kind lexeme)
                  '(:header :ident :number
                            :char :string
                            :punctuator :other))
       t))

Theorem: booleanp-of-plexeme-tokenp

(defthm booleanp-of-plexeme-tokenp
  (b* ((yes/no (plexeme-tokenp lexeme)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: plexeme-tokenp-alt-def

(defthm plexeme-tokenp-alt-def
 (equal
      (plexeme-tokenp lexeme)
      (not (member-eq (plexeme-kind lexeme)
                      '(:block-comment :line-comment :newline
                                       :spaces :horizontal-tab
                                       :vertical-tab :form-feed)))))

Theorem: plexeme-tokenp-of-plexeme-fix-lexeme

(defthm plexeme-tokenp-of-plexeme-fix-lexeme
  (equal (plexeme-tokenp (plexeme-fix lexeme))
         (plexeme-tokenp lexeme)))

Theorem: plexeme-tokenp-plexeme-equiv-congruence-on-lexeme

(defthm plexeme-tokenp-plexeme-equiv-congruence-on-lexeme
  (implies (plexeme-equiv lexeme lexeme-equiv)
           (equal (plexeme-tokenp lexeme)
                  (plexeme-tokenp lexeme-equiv)))
  :rule-classes :congruence)