		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Plexeme-token/space-p

Check if a preprocessing lexeme is a token or a (single) space.

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

This is used to represent, and facilitate comparison of, replacement lists of macros, as explained in more detail elsewhere.

Definitions and Theorems

Function: plexeme-token/space-p

(defun plexeme-token/space-p (lexeme)
  (declare (xargs :guard (plexemep lexeme)))
  (or (plexeme-tokenp lexeme)
      (and (plexeme-case lexeme :spaces)
           (equal (plexeme-spaces->count lexeme)
                  1))))

Theorem: booleanp-of-plexeme-token/space-p

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

Theorem: plexeme-token/space-p-of-plexeme-fix-lexeme

(defthm plexeme-token/space-p-of-plexeme-fix-lexeme
  (equal (plexeme-token/space-p (plexeme-fix lexeme))
         (plexeme-token/space-p lexeme)))

Theorem: plexeme-token/space-p-plexeme-equiv-congruence-on-lexeme

(defthm plexeme-token/space-p-plexeme-equiv-congruence-on-lexeme
  (implies (plexeme-equiv lexeme lexeme-equiv)
           (equal (plexeme-token/space-p lexeme)
                  (plexeme-token/space-p lexeme-equiv)))
  :rule-classes :congruence)